\chapter{面向大规模网络的数据平面模型构建研究}
\label{cha:model}
本章主要聚焦于面向大规模网络的数据平面模型构建研究。首先，通过分析已有研究工作发现了在大规模网络中普遍存在的“更新风暴”现象，提出了提高数据平面模型构建吞吐量和伸缩性的问题。然后，探讨了“更新风暴”所涉及的数据平面更新的非原子性和谓词并发操作挑战。接着，提出了面向大规模网络的数据平面验证系统Flash，Flash采用了快速逆模型变换（FIMT）和并行流水线的数据平面模型构建方法，显著提高数据平面模型构建的效率。最后，在真实大规模网络上的实验表明，相对于最新的已有工作，Flash在数据平面模型构建效率方面的提升高达40,000倍。

\cref{fig:model-outline}列出了面向大规模网络的数据平面模型构建研究路径。\cref{sec:model-bg}描述了面向大规模网络的数据平面模型构建研究背景，在\cref{sec:model-problem}中，对数据模型快速构建需要解决的问题和直观思路进行描述，在\cref{sec:model-challenge}中提出直观思路所面临的挑战，在\cref{sec:model-solution-fimt}和\cref{sec:model-solution-par}中针对挑战提出相应的解决方案，并在\cref{sec:model-eval}中对所提出的解决方案进行实验验证。

\begin{figure}[]
  \centering
  \includegraphics[width=\textwidth]{figures/model/outline.pdf}
  \caption{面向大规模网络的数据平面模型构建研究路径}
  \label{fig:model-outline}
\end{figure}

\section{面向大规模网络的数据平面模型构建研究背景}
\label{sec:model-bg}
实现可验证路由编程的首要任务是实现验证平面的数据平面验证系统，而数据平面验证的关键步骤之一是构建能够利于实现高效验证的数据平面模型（Data plane model），数据平面模型是描述网络设备数据平面行为的抽象模型，也是验证算法的输入之一，决定了验证算法的具体实现，同时，数据平面模型的构建速度直接影响验证系统的效率。因此，快速构建数据平面模型是实现高效的可验证路由编程系统的关键。

% \subsection{数据平面的更新风暴现象}
\textbf{数据平面的“更新风暴”（Update storm）现象。}随着计算机网络规模和复杂性的增长~\cite{singh2015jupiter}，在真实网络和大规模网络仿真中，由单一原因触发大量数据平面更新并不罕见。本文将短时间内收到大量数据平面更新的情况称为“更新风暴”（Update storm）。例如已有工作~\cite{holterbach2017swift}表明互联网拓扑中的单一链路状态变化可以引发大量的BGP路由变化，并导致域内网络中FIB的大量更新。

首先，域间的链路变化可能导致大量的FIB更新。考虑~\cref{fig:s0a}所示的BGP网络，假设它从Internet接收到10K个IP前缀，并且对于域内IGP网络这10K个前缀的最佳路径是通过边界路由器A转发，如图~\ref{fig:s0a}所示。在域间链路发生故障后，前缀将从A中撤回，新的最佳路径是通过路由器B转发数据包，如~\cref{fig:s0b}所示。即使对于一个包含3个节点的拓扑，这个变化将触发10K个FIB更新。

其次，域内的链路变化也可能触发大量的FIB更新。考虑\cref{fig:s0c}所示的网络，当从C到B建立一个新的链路时，域内的最优路径从C - A - B - Internet变为C - B - Internet（假设域内运行OSPF，且链路权重都相同）。因此，对于Internet所宣告的前缀，设备C将触发10K次更新。本文使用FRR\cite{FRR}评估了\cref{fig:storm0}中的情景，\cref{fig:storm-dist}显示了在触发链路事件时更新的累积数量。当链路A-Internet故障时，在0.48秒内从A接收到10K
% \footnote{当链路A-Internet故障时，还从C接收到了10,000个FIB更新，但是这些更新没有改变其原始FIB，因此没有报告这些更新。}
次突发更新，而在1.36秒时设置链路B-C后，在0.58秒内从C接收到10K次突发更新。

除了上述情况外，网络仿真~\cite{liu2017crystalnet, lopes2019fast, fogel2015general,
abhashkumar2019tiramisu, quoitin2005modeling}工具也会在短时间产生大量的FIB更新。最先进的网络仿真工具，如FastPlane~\cite{lopes2019fast}，可以在几百秒内计算出超过2,000个路由器组成的网络的FIB，且FIB的规模可以达到数亿条。例如，考虑图\ref{fig:storm1}所示的情景，假设网络采用$K$-Fattree拓扑，每个POD具有$P$个前缀，$|R|$为变化后的总规则数，$|\Delta R|$为修改的规则数。当$K=32$且$P=32$时，向数据中心网络中添加一个新的POD时，仿真工具将生成1,310,720个FIB规则和71,680次FIB变化。

将这些FIB条目输入到数据平面验证器中会导致\textbf{很长的验证时间}和\textbf{大量的内存消耗}。即使对于增量式数据平面验证器来说~\cite{kazemian2013real, zhang2020apkeep, horn2017deltanet}，大量的FIB更新也会导致性能问题。虽然可以采用分而治之的方法如Libra~\cite{zeng2014libra}，但数据平面的复杂性带来的分区难度可能非常高。例如，在一个具有约6,000个交换机的数据中心拓扑中的FIB更新数据集中，即使将头部空间划分为112个分区，对于现有最先进的数据平面验证器（如APKeep~\cite{zhang2020apkeep})也需要花费几十分钟到几小时的时间来完成对一个分区的验证（如\cref{sec:model-eval}实验结果所示）。

\begin{figure}[t]
  \centering
  \begin{subfigure}[t]{0.27\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{model/motivation-storm0.pdf}
    \caption{初始状态}
    \label{fig:s0a}
  \end{subfigure}
  \begin{subfigure}[t]{0.27\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{model/motivation-storm1.pdf}
    \caption{域间链路故障}
    \label{fig:s0b}
  \end{subfigure}
  \begin{subfigure}[t]{0.27\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{model/motivation-storm2.pdf}
    \caption{域内链路恢复}
    \label{fig:s0c}
  \end{subfigure}
  \caption{域间/域内路由中的更新风暴示例}
  \label{fig:storm0}
\end{figure}
\begin{figure}
    \centering
    \includegraphics[width=.7\linewidth]{model/bgp-test.png}
    \caption{数据平面更新的累积数量}
    \label{fig:storm-dist}
\end{figure}

\begin{figure}
  \centering
  \begin{subfigure}{.55\linewidth}
    \includegraphics[width=\linewidth]{model/storm-new-pod.pdf}
  \end{subfigure}
  \begin{subfigure}{.38\linewidth}
    \footnotesize
    \begin{tabular}{llll}
      \emph{K} & \emph{P} & \emph{$|R|$} & \emph{$|\Delta R|$} \\\hline
      4 & 2 & 160 & 56 \\
      8 & 4 & 2,560 & 512 \\
      16 & 8 & 40,960 & 4,352 \\
      32 & 16 & 655,360 & 35,840 \\
      32 & 32 & 1,310,720 & 71,680 \\
    \end{tabular}
  \end{subfigure}
  \caption{网络规划中的更新风暴：将新的POD连接到数据中心网络}
  \label{fig:storm1}
\end{figure}

造成已有数据平面验证工具（如APKeep~\cite{zhang2020apkeep}，DeltaNet~\cite{horn2017deltanet}等）在“更新风暴”现象下效率低下的主要原因在于它们\textbf{关注于单一FIB更新的处理}，虽然其效率已达到微秒级，但是在大规模网络情况下，数据平面更新往往是批量化、爆发式发生，大量的FIB更新依然会导致性能的下降，尤其是在初始化阶段，验证系统会收到大量的已有网络设备数据平面配置数据，每次处理一个更新无疑是非常低效的方式。因此，在这样的背景下，本文进行了面向大规模网络的数据平面模型构建研究。

% 如图~\ref{fig:fattree} 所示为Fattree网络规模及其数据平面规则数量关系，其中横轴$P$为每个ToR(Top of Rack)上分配的IP地址，纵轴\#Updates为数据平面配置总数，不同的线条表示Fattree网络的Pod数量。由于$\#Updates = O(K^4 \times P)$，随着$K$和$P$增加，数据平面规则数量将呈次方级增加。



% \begin{figure}[htbp]
%   \centering
%   \includegraphics[width=.7\textwidth]{model/fattree.png}
%   \caption{Fattree网络规模和数据平面规则数量关系}
%   \label{fig:fattree}
% \end{figure}

% \subsection{面向大规模网络的数据平面模型构建研究路径}


% “更新风暴”在实际网络中是一个普遍存在的现象，验证系统需要能够短时间内快速处理大量的数据平面更新，才能保证验证结果的时效性，如何在“更新风暴”情况下实现快速高效的数据平面构建是数据平面验证中的关键挑战之一。\cref{fig:model-outline}列出了数据平面模型快速构建研究的主要问题、挑战和方案。在\cref{sec:model-problem}中，对数据模型快速构建需要解决的问题进行描述，在\cref{sec:model-challenge}中，提出解决问题所面临的挑战，在\cref{sec:model-solution-fimt}和\cref{sec:model-solution-par}中针对挑战提出相应的解决方案，并在\cref{sec:model-eval}中对所提出的解决方案进行实验验证。




% \textbf{数据爆炸问题}。FIB的match域所表示的包头空间通常情况下会非常大，比如IP前缀10.0.0.0/8表示了$2^{24}$个包含元素的包头空间，这会导致验证系统无法在有限的存储空间和时间内处理大量的包头空间，本文必须将包头空间及其操作映射为一个更加有效的数据空间，从而降低空间和时间复杂度。

% \textbf{模型构建效率问题}。

\section{面向大规模网络的数据平面模型构建问题描述}
\label{sec:model-problem}



% 在等价类表示中，$C$的转发行为可以表示为一个函数：
% \[
% \vec{b}_{M}^C(h) = \vec{y}^{j^*}，\text{ 其中 } p^{j^*}(h) = 1。
% \]

% \subsection{数据平面模型快速构建主要研究问题}
为了应对大规模网络中的“更新风暴”现象，数据平面验证系统需要能够在短时间内完成对大量数据平面更新的处理，为了精确描述问题，本节首先对数据平面验证所涉及的基本对象进行抽象化描述。

\textbf{网络拓扑抽象。}
一个物理网络包含多个设备，设备之间通过物理链路连接，由于任意两个设备之间可能存在多条物理链路，且对于任意一条链路，不同的数据传输方向具有不同的特性（如：带宽、延迟和权重等），所以网络拓扑可以抽象为一个有向多边图 (Directed multigraph) $G(D,L)$，其中$D$为所有网络设备和终端主机集合，符号$term(D) \subseteq D$表示所有的终端设备，$net(D) \subseteq D$表示所有的网络设备（如路由器和交换机），终端设备负责产生和接收数据包，网络设备负责转发数据包。

每个设备$d \in D$具有多个物理端口$\Psi_d=\{\psi_1^d,...,\psi_{|\Psi_d|}^d\}$，其中$\psi_i^d$表示设备$d$的第$i$个端口。令$\Omega=\bigcup_{d \in D}\Psi_d$为网络中所有端口集合, 则$L \subseteq \Omega \times \Omega$为该有向多边图$G$的边集合，每条有向边$(\psi^u_i, \psi^v_j) \in L$表示网络中存在一条从设备$u$的第$i$个端口到设备$v$的第$j$个端口的链路，由于本文针对的链路为全双工链路，所以$|L|$为偶数，换言之，如果$(\psi^u_i, \psi^v_j) \in L$，则$(\psi^v_j, \psi^u_i) \in L$。在上下文清楚的情况下，本文用$\psi$表示一个端口。

另外，本文用$dev(\psi)$表示端口$\psi$所属的设备，$peer(\psi)$表示与端口$\psi$连接的对端端口，$pdev(\psi) = dev(peer(\psi))$表示对端端口所属的设备。对于一条链路$l=(\psi_i, \psi_j) \in L$，本文用$src(l) = \psi_i$和$dst(l) = \psi_j$分别表示有向边$l$的开始和结束端口，$srcd(l) = dev(\psi_i)$和$dstd(l) = dev(\psi_j)$表示$l$所连接的开始和结束设备。

\textbf{网络数据包抽象。}
网络数据包由一个数据包头$h$和数据包内容构成，本文主要关注网络数据包头，定义数据包头如下：
\begin{definition}
  \textbf{数据包头($h$)：}一个数据包具有一个固定长度的比特序列数据包头$h \in \{0,1\}^{|h|}$，其中$|h|$为数据包头长度。
\end{definition}

由于网络往往根据特定的路由协议工作，路由协议只关心其对应数据包头的某一部分，在没有特别说明情况下，本文中的数据包头指代路由协议相关部分，比如在一个基于目的IP地址转发的IPv4路由网络中，目的地址为1.2.3.4的数据包头为$h=\{00000001\ 00000010\ 00000011\ 00000100\}$，本文用$\mathcal{L}$来表示协议对应的数据包头长度，如基于目的IP地址转发的IPv4路由网络中$\mathcal{L}=32$。同时，本文用符号$\mathbb{H}$表示协议所能表达的所有的数据包头集合，如在一个IPv4路由网络中，$\mathbb{H} = \{0,1\}^{32}$。为了简化表示，在上下文清楚的情况下，本文也使用IP地址来表示一个数据包头（如10.0.0.1）。



\begin{definition}
  \textbf{包头空间($H$)：}多个数据包头的集合构成一个包头空间$H=\{h_1,...,h_{|H|}\}$，其中$|H|$为该包头空间包含的数据包头数量，且$\forall i \neq j: h_i \neq h_j$。
\end{definition}

在IP路由网络中，网络通常会划分为多个子网，子网用IP地址和子网掩码构成，网络设备也通常用IP prefix来定义路由规则，而一个IP prefix定义了一个包头空间，如IPv4地址前缀10.0.0.0/24对应于一个包含$2^8$个数据包头的包头空间$\{10.0.0.0,...,10.0.0.255\}$。另外，定义函数$H(h): \mathbb{H} \rightarrow Bool$表示数据包头$h$是否存在于包头空间$H$。为了简化表示，在上下文清楚的情况下，本文也使用IP地址前缀来表示一个包头空间（如10.0.0.0/24）。

\textbf{数据平面行为抽象。}
网络的数据平面决定了网络设备如何处理进入网络的数据包。具体来说，给定一个物理网络$G(D,L)$, 每个网络设备$d \in net(D)$包含一套转发信息表（FIB）$R_d$，其中包含一系列数据包转发规则$R_d = \{r_1,...,r_{|R_d|}\}$，每条规则$r\in R_d$可抽象为一个三元组$\langle pri_r, match_r, action_r \rangle$（为了精简表达，在上下文清楚的情况下，本文也使用$\langle pri_r, m_r, a_r\rangle$表示规则元素）, 其中$pri_r \in \mathbb{Z}$为该规则的优先级（本文约定$pri_r$越大优先级越高），$m_r \in \{0,1,\text{x}\}^\mathcal{L}$为数据包头的匹配值，x为任意匹配，$a_r$为对应的动作，如转发、多播、广播或者丢弃。FIB的语义如下，对于进入网络设备$d$的具有包头为$h$的数据包，对于规则$r \in R_d$，如果$m_r$域能够匹配$h$，且$pri_r$是匹配$h$的最高优先级规则，则使用规则$a_r$来处理该数据。为了精简表达，在上下文清楚的情况下，本文也使用$field=val$列表来表示一个match域（如$m_r := [dstIP=10.0.0.0/24]$）。

\textbf{单个网络设备数据平面的行为抽象。}给定一个网络设备$d$，对于一条转发规则$r \in R_d$，$m_r$本质上是一个包头空间，如基于目的IP的路由为了中，$m_r := [dstIP=10.0.0.0/24]$对应于包头空间$H_r = \{10.0.0.0,...,10.0.0.255\}$。另外，$a_r$决定了数据包的处理，如$a_r := forward(eth0)$表示将数据包转发到eth0。基于上述抽象，一个网络设备基于其转发信息表$R_d$处理数据包的过程可以抽象为一个函数$F_d: \mathbb{H} \rightarrow A_d$，其中$A_d=\{a_r|r \in R_d\}$为$R_d$所有action的集合，定义如下：

\begin{equation}
  F_d(h) = a_r, \text{其中}r = \mathop{\arg\max}\limits_{H_r(h)=True, r \in R_d}pri_r
\end{equation}

\textbf{整体网络数据平面的行为抽象。}基于单个设备的数据平面行为抽象，整体网络数据平面的行为可抽象为一个迭代函数。本文定义整体网络数据平面的行为如下：

\begin{equation}
  \mathcal{F}_\mathcal{R}(d, h) = \{F_{d_1}(h), F_{d_2}(h),...,F_{d_N}(h)\}
\end{equation}
其中$\mathcal{R}$为所有设备的数据平面配置集合，且$d_i = pdev(F_{d_{i-1}}(h)), i \in [1,N]$。$\mathcal{F}_\mathcal{R}(d, h)$表示给定数据平面配置$\mathcal{R}$，当数据包头为$h$的数据包通过设备$d$进入网络时，$\mathcal{F}_\mathcal{R}$返回数据包经过设备的匹配规则的动作集合。如果不指定初始设备$d$，$\mathcal{F}$返回所有网络设备对于包头$h$的动作，网络的整体行为定义为：

\begin{equation}
  \mathcal{F}(h, \mathcal{R}) = \{F_{d}(h) | d \in net(D)\}
\end{equation}

给定一个数据平面$DP(G, \mathcal{R})$，其中$G(D,L)$为网络拓扑，$\mathcal{R}=\{R_d|d\in net(D)\}$为数据平面FIB集合，数据平面验证的关键步骤是建立描述数据平面行为的数据平面模型，数据平面模型具体定义如下：


\begin{definition}
  \label{def:dpm}
  \textbf{数据平面模型}。给定一个数据平面$DP$，其数据平面模型$M$为一个元组$M\langle V,A,\Sigma,\delta \rangle$，其中:
\end{definition}

\begin{enumerate}
  \item $V$为节点集合，包括所有网络设备$D$和一个虚拟节点$\var{DROP}$；
  \item $A \subseteq V \times V$为有向边集合，对应网络中所有的物理连接和物理设备到DROP设备的连接；
  \item $\Sigma \subseteq 2^\mathbb{H}$为包头空间构成的集合；
  \item $\delta$: $A \rightarrow 2^\Sigma$为从边集合到包头空间集合的映射。
  % \item $\lambda$: $\mathbb{H} \rightarrow \Sigma$为数据包头到标签的映射。
\end{enumerate}
令$A_v^{out}$表示节点$v$的所有出边，数据平面模型需满足以下性质：
\begin{itemize}
  \item 包头空间非空：$\forall H \in \Sigma: H \neq \emptyset$；
  \item 包头空间唯一性：$\forall H_i,H_j \in \Sigma: H_i \neq H_j$；
  \item 包头空间完备性：$\bigcup_{H \in \Sigma}H = \mathbb{H}$；
  \item 节点转发完备性：对于任一节点$v \in V$，$\bigcup_{e \in A_v^{out}}\delta(e) = \mathbb{H}$；
  \item 单播（unicast）节点转发互斥性：对于只有unicast规则的节点$v$，还需满足 $\forall e_i, e_j \in A_v^{out}: \bigcup_{H \in \delta(e_i)}H \cap \bigcup_{H \in \delta(e_j)}H = \emptyset$。
\end{itemize}

数据平面模型本质为一个带有标签的有向图，对于任意节点$v \in V$，当数据包头为$h$的数据包进入$v$，该节点通过边$\mathcal{F}(v, h)$发往下一跳，其中：
\begin{equation}
  \mathcal{F}(v, h) = \{e|h \in \bigcup_{H \in e}H, e \in A_v^{out}\}
\end{equation}

数据平面验证的正确性依赖于数据平面模型的正确性，如果数据平面模型本身是错误的，则基于该数据平面的验证将毫无意义，即数据平面模型必须与数据平面配置等价，本文定义数据平面模型的等价性如下。
\begin{definition}
  \textbf{数据平面模型的等价性}。给定一个数据平面$DP$以及数据平面模型$M$，如果对任意具有数据包头$h$的数据包从网络设备$d$进入网络，$F(d, h) = \mathcal{F}(d, h)$，则称该$M$与$DP$等价，表示为$M \sim DP$。
\end{definition}

对于大规模网络，短时间内可能会有大量的数据平面更新，如果不能及时处理这些数据平面更新，会造成验证结果严重滞后。尤其在高速网络环境中，网络设备能够处理大量的数据包，验证系统必须在极短的时间内做出正确的决策，否则会有大量“非法”数据被传输。具体而言，在“更新风暴”情况下实现数据平面模型的快速构建需要研究以下问题：

% 实现快速数据平面模型构建需要实现高效地前向模型到逆向模型的变换，本文的数据平面模型采用基于原子谓词的数据平面模型，由于构建基于原子谓词的数据平面模型需要大量的包头操作，在“更新风暴”情况下依然保证数据平面模型的构建效率是一个挑战。具体而言，实现数据平面模型快速构建需要研究的问题如下：

\textbf{P1: 如何提高数据平面模型构建的吞吐量。}
数据平面模型构建的目标为给定数据平面$DP(G, \mathcal{R})$和等价的数据平面模型$M \sim DP$，当数据平面发生更新$\Delta \mathcal{R}$，数据平面验证系统需要构建新的数据平面模型$M'$，使得$M' \sim DP(G, \mathcal{R} + \Delta \mathcal{R})$，其中$\mathcal{R} + \Delta \mathcal{R}$表示数据平面规则集合合并\footnote{$\mathcal{R}$中包括增加或删除规则，对应为集合元素的增加和删除}。同时定义数据平面模型构建的吞吐量为$|\Delta \mathcal{R}|/t$，单位为“更新每秒”（Updates per second, ups），其中$|\Delta \mathcal{R}|$为验证系统收到的数据平面更新数量，$t$为从收到$|\Delta \mathcal{R}|$的第一个数据平面更新到更新全部处理完成的时间。所以，如何提高数据平面模型构建的吞吐量是数据平面验证系统的关键问题之一。



\textbf{I1: 批量化处理数据平面更新。}为了提高数据平面模型构建过程的吞吐量，直观思路是通过批量化方式处理数据平面更新。批量化处理数据平面更新意味着通过“批处理”方式每次处理一组更新，通过对一组更新进行分析和聚合，从而降低数据平面模型构建过程的输入规模，提高数据平面模型构建的吞吐量。具体而言，采用批处理方式可以带来以下好处。首先，批量化处理数据平面更新能够避免无效更新，从而消除冗余的数据平面更新条目，如\cref{fig:model-int-red}所示的例子，在一个简单的二层网络中配置LSW1和LSW2的聚合链路过程中\footnote{案例假设STP未启用，且所有接口属于同一个VLAN}，由于配置过程的延迟（两条链路启用到聚合链路配置成功的时间间隔），LSW1和LSW2之间会产生短暂的环路，直到聚合链路配置成功，此时PC1到PC2的流量将在LSW1和LSW2形成的环路中循环，导致LSW1不断地更新其MAC地址表，如\cref{fig:model-int-red}表格所示，如果将MAC地址表的更新作为一组更新分析，会发现唯一有效的更新为最后一个条目，之前所有的更新被最后一个条目覆盖，那么可以直接将所有无效条目删除后再对数据平面模型进行更新。其次，批量化处理数据平面更新可以实现更新的聚合，如\cref{fig:model-int-agg}所示的例子，对于具有相同出端口的IPv4路由更新条目可以聚合为一条更新，从而降低数据平面更新过程的输入规模。


\textbf{P2: 如何提高数据平面模型构建的伸缩性。} 现代硬件往往具备多核结构，验证系统需要能够充分利用多核结构从而实现更高效的验证过程。而已有工作（如APKeep\cite{zhang2020apkeep}，Delta-net\cite{horn2017deltanet}等）只能以单线程模式运行，这样的方式极大地限制了验证系统的伸缩性。因此，在大规模网络验证中，提高数据平面模型构建的伸缩性也是一个关键研究问题。


\textbf{I2: 并行化处理数据平面更新。}为了提高数据平面模型构建过程的伸缩性，直观思路是通过并行方式处理数据平面更新。并行化处理数据平面更新意味着对所有数据平面更新进行并行处理，从而充分利用硬件资源，提高数据平面模型构建过程的伸缩性。例如，在\cref{fig:model-int-agg}的例子中，可以采用Map-GroupBy-Reduce方式实现并行聚合过程，首先对所有数据平面更新用Map过程并行计算前缀对应的谓词表达，然后对结果集合按照Inteface进行分组，最后对同一组内的条目并行进行“逻辑或”谓词聚合操作。另外，对于批处理过程中多个批也可以通过并行方式分别进行计算，并使用与服务器CPU核心数量相同大小的线程池，可以充分利用服务器多核资源，提高数据平面模型构建过程的伸缩性。

% 然而基于AP的数据平面模型并未考虑网络拓扑，会导致原始谓词列表被过度划分，进而影响之后的验证过程。以图~\ref{fig:lep-topo}为例，图中所示为一个示例网络及其数据平面配置，该网络包含3个设备，其中设备B和C分别与外部网络Ext 1和Ext 2连接。图~\ref{fig:lep-over-partition}为使用atomic predicates计算得到的数据平面模型。

% 令函数$C$为数据平面模型构建函数，该函数输入一个数据平面，输出对应的数据平面模型，令$M=C(DP)$，数据平面模型构建问题为找到函数$C$，使得$M$满足数据平面模型正确性。


% \section{面向大规模网络的数据平面模型构建直观思路}
% \label{sec:model-intuition}



\begin{figure}[t]
  \centering
  \begin{subfigure}[t]{0.52\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{figures/model/int-redundant.png}
    \caption{批量化处理数据平面更新避免无效更新}
    \label{fig:model-int-red}
  \end{subfigure}
  \begin{subfigure}[t]{0.35\linewidth}
    \centering
    \includegraphics[width=1\linewidth]{figures/model/int-agg.png}
    \caption{对数据平面更新聚合}
    \label{fig:model-int-agg}
  \end{subfigure}
  \caption{批量化处理数据平面更新示例}
\end{figure}


\section{面向大规模网络的数据平面模型构建的挑战}
\label{sec:model-challenge}

虽然批量化和并行化处理数据平面更新的直观思路简单直接，然而，在实际的数据平面更新处理过程中并非易事，简单的对数据平面处理会导致错误的计算结果，具体而言，实现批量化和并行化处理数据平面更新主要面临以下挑战：

\begin{figure}[]
  \centering
  \includegraphics[width=\textwidth]{figures/model/non-atomic.png}
  \caption{直接合并数据平面更新导致错误的数据平面模型}
  \label{fig:model-non-atomic}
\end{figure}

\textbf{C1:数据平面更新的非原子性。}在处理一组更新时，简单地合并数据平面更新可能造成不正确数据平面模型。例如，在\cref{fig:model-non-atomic}所示的例子中，$\mathcal{R}$是使用最长前缀匹配的IPv4网络的数据平面，并且每个设备有两条规则。网络中有两个等价类，当在每个设备上插入如$\Delta \mathcal{R}$所示的三条规则时，如果直接将具有相同action的规则进行合并，得到的数据平面模型是错误的。

另外，合并每条数据平面更新对应的数据平面模型更新也会导致错误的数据平面模型。例如，在\cref{fig:model-non-atomic1}所示的例子中，首先计算每个规则更新对应的数据平面模型更新，如果合并最后两个模型更新，因为它们具有相同的网络行为，应用这些模型更新仍将得到一个错误的模型，原因是这些数据平面模型更新是非原子性的（Not conflict-free），数据平面模型更新的match域对应的包头空间之间存在重叠，因此不能简单地组合这些数据平面模型更新。

\begin{figure}[]
  \centering
  \includegraphics[width=\textwidth]{figures/model/non-atomic1.png}
  \caption{合并数据平面模型更新导致错误的数据平面模型}
  \label{fig:model-non-atomic1}
\end{figure}

\textbf{C2: 数据平面更新并行处理的顺序随机性。}虽然并行化处理数据平面更新能够带来效率和伸缩性上的提升，但是简单的对数据平面更新进行并行处理可能因执行顺序的随机性导致错误的计算结果。例如在\cref{fig:model-cha-order}所示的例子中，当数据平面更新被分为了两个不同的批（Batch），两个批被并行处理，如果Batch 2先完成，则Batch 2的更新会被Batch 1覆盖，最终导致错误的计算结果。

\begin{figure}[]
  \centering
  \includegraphics[width=\textwidth]{figures/model/challenge-order.png}
  \caption{数据平面更新并行处理的顺序随机性示例}
  \label{fig:model-cha-order}
\end{figure}

\textbf{C3: BDD并发操作的不一致性。}二叉决策图（Binary Decision Diagram，BDD）因其简单易用、内存高效以及能够以简洁的方式表达复杂的转发规则而在主流数据平面验证系统中得到广泛应用，基于BDD构建的数据平面模型可以简单地用谓词对应的BDD根节点ID来表示一个等价类，从而使验证过中的包头操作变为简单的整数集合操作。然而，BDD节点的唯一性也带来了BDD并发操作的不一致性问题。例如，给定以下两个BDD操作，$p_a = p_1 \wedge p_2$和$p_b = p_1 \wedge \neg p_2$，当$p_1$对应的BDD节点尚未被构建，则需要递归地构建$p_1$对应的BDD根节点，当两个操作并发执行时，会创建两个$p_1$对应的BDD节点，破坏了BDD结构的唯一性，此时，如果计算$p_a \vee p_b$，结果应该为$p_1$，而此时BDD中存在两个$p_1$节点，系统无法确定应该使用哪一个节点，不同的计算方式会导致返回不同的结果，本文将上述问题称为\textbf{BDD并发操作的不一致性}。

在BDD算法库方面，主流的数据平面验证工具采用BDD作为核心数据结构~\cite{yang2016realtime, yang2017scalable, guo2022flash, zhang2020apkeep, zhang2022differential, xiang2022network}，从而实现有效地表示和验证数据平面模型。然而，现有的基于BDD的数据平面验证系统主要关注减少BDD操作的数量，而缺乏对底层BDD库的伸缩性优化。例如，APKeep通过采用谓词拆分和延迟合并技术来减少冗余的BDD操作，而Flash则通过批处理来消除重复的BDD操作。然而，这些方法都采用了单线程的BDD包，限制了系统的伸缩性。对于大规模网络而言，实现大规模数据平面验证对于具备可伸缩性的BDD基础设施的需求迫切。因此，需要一个能够支持大规模数据平面验证的BDD基础设施来满足这一需求。

截止该论文提交之前，在迭代开发Flash~\cite{guo2022flash}的过程中调研尝试了多种当前可用的BDD库及其相关文献，现有的通用BDD库在支持数据平面验证的伸缩性方面表现不佳。本文调查了表~\ref{tab:bdd-libs} 中列出的各种公开可用的BDD库。如BuDDy~\cite{jorn2023buddy}、CUDD~\cite{fabio1999cudd}和JDD~\cite{vahidi2023bdd}这样的单线程库不支持线程安全的并行操作。BeeDeeDee~\cite{lovato2014threadsafe}使用基于互斥锁的结构进行多线程BDD操作，这妨碍了多核系统的有效利用。PJBDD~\cite{beyer2021pjbdd}和Sylvan使用线程池和无锁数据结构进行并行BDD操作，但它们在每个操作中使用了\emph{fork-join} (FJ)方案（即使用多个线程处理单个递归BDD操作），与\emph{run-to-completion} (RtC)方案相比，导致更大的开销。此外，Sylvan中的线程池缺乏可重新调度性，导致处理大规模数据平面更新时出现死锁并耗尽可用线程。HermesBDD~\cite{capogrosso2023hermesbdd}采用按需线程创建方法实现高伸缩性，但在高负载的BDD操作中会面临线程调度开销和过度线程创建的问题。总体而言，本文认识到现有BDD包的不适用性的根本原因是\textbf{现有通用BDD库的目标是加速单个BDD操作，而不是提高处理大量BDD操作的整体吞吐量}。在支持高伸缩性的数据平面验证方面，现有的通用BDD库表现不佳。另外，大部分库都提供了BDD节点自动引用（Automatic reference）功能，从而降低了程序中的内存泄露风险。

% 如JDD，BuDDy，BeeDeeDee，Sylvan等，已有系统均不能满足性能需求，表~\ref{tab:bdd-libs} 列出了已有可用的BDD库及其特性，其中BuDDy, CUDD, JDD为单线程库，无法支持线程安全(Thread-safe)的并行操作，PJBDD和BeeDeeDee使用基于互斥锁的结构实现多线程BDD操作，然而基于互斥锁的结构每一时刻只允许允许一个BDD操作，无法充分利用多核并行。Sylvan和HermesBDD实现了一定的基于无锁(Lock-free)结构的并行BDD操作，HermesBDD同时实现了缓存的无锁并行操作，然而，HermesBDD使用同步方式按需创建线程，当大量BDD操作发生时，HermesBDD会产生大量的线程创建和销毁工作，性能会急剧下降。Sylvan使用线程池来降低线程创建开销，然而在大量BDD操作并发时，线程池会迅速耗尽最后导致死锁（Dead-lock），因此无法在大规模数据平面更新情况下得到计算结果。


\begin{table}[]
  \center
  \caption{现有可用的BDD库及其特性}
  \label{tab:bdd-libs}
  \resizebox{\linewidth}{!}{
  \begin{tabular}{|c|c|c|c|c|c|c|}
    \hline
    \emph{名称}
    & \emph{语言}
    & \emph{线程安全}
    & \emph{死锁安全}
    & \makecell[c]{\emph{无锁节点表}}
    & \makecell[c]{\emph{无锁缓存}}
    & \makecell[c]{\emph{自动引用}}
    \\\hline
    BuDDy~\cite{jorn2023buddy} & C/C++ & N & - & N & N & Y
    \\\hline
    CUDD~\cite{fabio1999cudd} & C++ & N & - & N & N & Y
    \\\hline
    JDD~\cite{vahidi2023bdd} & Java & N & - & N & N & N
    \\\hline
    PJBDD~\cite{beyer2021pjbdd} & Java & Y & Y & N & Y & Y
    \\\hline
    BeeDeeDee~\cite{lovato2014threadsafe} & C++ & Y & Y & N & N & Y
    \\\hline
    Sylvan~\cite{tomvandijk2017sylvan} & C++ & Y & N & Y & N & Y
    \\\hline
    HermesBDD~\cite{capogrosso2023hermesbdd} & C++ & Y & N & Y & Y & Y
    \\\hline
  \end{tabular}
  }
\end{table}

% \subsection{数据平面行为抽象}
% 网络的数据平面能够对进入网络的数据包进行转发和变换操作，本文称该过程位网络数据平面的动态行为。为了形式化描述网络的动态行为，本文定义以下基本概念。

% \begin{definition}
%   包头空间$H$: 数据包头空间$H$是由$\{0,1\}^L$构成的一个包头集合，其中$L$为数据包的头部长度。
% \end{definition}

% 令$\mathbb{H}$为所有可能的包头构成的全集，对于数据包头空间$H_1,H_2\in \mathbb{H}$，本文定义以下操作符：

% \begin{equation}
% \begin{split}
%   H_1 \times H_2 = H_1 \wedge H_2\\
%   H_1 + H_2 = H_1 \vee H_2
% \end{split}
% \end{equation}


% 显然$2^\mathbb{H}$构成一个环$\langle 2^\mathbb{H},\times,+\rangle$，根据集合的代数特性，上述操作符满足交换律、结合律和分配律：
% \begin{equation}
% % \begin{gather*}
% \begin{split}
%   H_1 \times H_2 = H_2 \times H_1 \\
%   H_1 + H_2 = H_2 + H_1 \\
%   H_1 \times H_2 \times H_3=H_1 \times (H_2 \times H_3 )\\
%   H_1+H_2+H_3=H_1+(H_2+H_3 )\\
%   H_1 \times (H_2+H_3 )=H_1 \times H_2+H_2 \times H_3
% \end{split}
% % \end{gather*}
% \end{equation}

% \begin{definition}
%   包头空间路由状态（header space routing state）LP:定义为一个二元组$\langle H,loc \rangle$，其中$H$为包头空间，$loc \in V$为当前网络位置。
% \end{definition}

% 数据平面的动态行为可以抽象为对包头空间路由状态的变换。

% \subsubsection{数据平面分布式验证的数据集抽象}
% 数据平面分布式验证的数据集可以抽象为一个key-value pair集合，其中key为一个三元组$key \in V \times \mathbb{Z} \times 2^\mathcal{H}$，而value为数据平面规则的动作。为了消除相同语义数据集的表达方式差异，数据集的键可以转换为谓词形式$key \in V \times \mathbb{P}$，从而消除了优先级。如图~\ref{fig:network}为一个包含三个设备的网络，各设备的FIB在图中列出，其对应的数据平面数据集抽象如图~\ref{fig:network-datset}所示。

% \begin{figure}[htbp]
%   \centering
%   \includegraphics[width=\textwidth]{example-network.pdf}
%   \caption{示例网络及其数据平面配置}
%   \label{fig:network}
% \end{figure}

% \begin{figure}[htbp]
%   \centering
%   \includegraphics[width=.4\textwidth]{example-network-dataset.pdf}
%   \caption{示例网络的数据集抽象}
%   \label{fig:network-datset}
% \end{figure}


% \subsection{基于流表结构的数据平面模型}
% 基于流表结构的数据平面模型直接使用流表结构作为

% \section{数据平面模型快速构建的挑战}
% 当前数据平面模型主要通过atomic predicates（AP）构建，然而，AP的计算只考虑了数据平面的FIB，并未考虑数据平面的拓扑链接情况，导致计算出来的AP存在“过度划分（Over-fine-grained）”问题。Atomic predicates定义如下：



% \begin{figure}[]
%   \centering
%   \includegraphics[width=0.8\textwidth]{lep-topo.pdf}
%   \caption{示例网络及其数据平面配置}
%   \label{fig:lep-topo}
% \end{figure}

% \begin{figure}[]
%   \centering
%   \includegraphics[width=0.8\textwidth]{lep-over-partition.pdf}
%   \caption{示例网络的atomic predicates数据平面模型}
%   \label{fig:lep-over-partition}
% \end{figure}

\section{基于批处理的数据平面模型构建方法}
\label{sec:model-solution-fimt}

本文提出了\textbf{S1: 基于批处理的数据平面模型构建方法}来解决挑战C1（数据平面更新的非原子性），该方法充分考虑了数据平面更新之间的相关性，将数据平面更新转换为原子覆写（Atomic overwrites）结构，基于MapReduce模型提出快速逆模型变换方法FIMT（Fast Inverse Model Transformation），并实现相应的系统Flash。



% 之后的内容首先介绍数据平面的逆模型结构，并通过示例阐述如何将规则更新转换为逆模型更新，然后提出基于MapReduce的快速逆模型变换过程。



数据平面模型所使用的数据结构决定了数据平面模型构建过程的目标，根据\cref{def:dpm}，其关键在于用何种数据结构表达包头空间集合$\Sigma$，对于数据平面模型的数据结构表达主要有两种方式，一种是前向模型（Forward model），另一种是逆向模型（Inverse model）。

\subsection{数据平面的前向模型表示}

网络数据平面的基于规则的表示记为$\mathcal{R}=\{R_i\}_{N}$，其中$R_i$表示第$i$个设备上的转发表。转发表由多个转发规则组成，格式为$\langle \var{pred}, \var{priority}, \var{action} \rangle$，其中\emph{pred}字段是一个\emph{谓词}（即数据包头空间上的布尔函数），\emph{priority}字段是一个整数，用于指定规则的优先级，而$\var{action}$表示要对数据包执行的操作（例如，转发、丢弃等）。

设$r_{ik}$表示第$i$个转发表中的第$k$条规则，$m_{ik}$、$\var{pri}_{ik}$和$a_{ik}$分别表示$r_{ik}$的匹配谓词、优先级和动作。
% $C$的转发行为是一个函数\footnote{这要求数据平面配置$C$没有由于具有模糊或冲突的转发规则而导致的语法错误，即两个具有重叠匹配、相同优先级但具有冲突动作的规则。这通常表示出现了错误，或者可以通过之前的工作（例如FlowVisor~\cite{sherwood2009flowvisor}）来解决。}：

\[
\vec{b}_{\mathcal{R}}(h) = (b_{1}(h), \dots, b_{N}(h)),
\]
其中第$i$个设备上的动作$b_i(h)$由可以匹配$h$的优先级最高的规则决定：
\[
b_i(h) = a_{ik^*}，\text{ 其中 } k^* = argmax_{r_{ik} \in R_i, m_{ik}(h) = 1} \var{pri}_{ik}。
\]

在如\cref{fig:model-fimt-example}所示的例子中，\cref{fig:model-fimt-example} 左上角标记为$\mathcal{R}$的表是三节点网络的FIB（基于规则的表示）示例。上方的表为三个交换机的转发信息表（FIB），分别用3列显示（即$R_i$是交换机$S_i$的FIB）。为了简化图示，图中用下一跳的设备作为动作，规则按优先级进行排序。为了说明如何解释该表，考虑一个示例数据包头$h_1$，其目的地IP地址为10.0.1.2。在设备$S_1$上，$R_1$中的规则$r_{11}$（$\langle \var{dip}=10.0.1.0/24, 2, A \rangle$）和规则$r_{13}$（$\langle \var{dip}=0.0.0.0/0, 0, S_3 \rangle$）都可以匹配该数据包，但规则$r_{11}$的优先级更高。因此，$b_{1}(h)$的输出是$A$。按照相同的步骤，在$S_2$（使用$R_2$）和$S_3$（使用$R_3$）上查找$h_1$，最终的输出是一个向量：$b_{\mathcal{R}}(h_1)=(A, S_1, S_1)$。

\begin{figure}[htbp]
  \centering
  \includegraphics[width=\linewidth]{figures/model/all-workflow.pdf}
  \caption{Flash数据平面模型构建过程示例}
  \label{fig:model-fimt-example}
\end{figure}

已有工作如HSA~\cite{kazemian2012header}和NetPlumber~\cite{kazemian2013real}所构建的数据平面模型为\cref{def:dpm}所定义数据平面模型的特例。由于这些工作可以看作是直接将FIB规则作为数据平面模型边集的标签，容易证明其构建的数据平面模型与数据平面是等价的。由于前向模型直接用转发规则的匹配域作为数据平面模型边集的标签，对于数据平面更新直接更新相应的转发规则即可，所以能够很好地应对“更新风暴”问题。然而，该模型直接存储大量的FIB，造成巨大的内存开销，而且在验证过程中需要进行大量的数据包头操作，导致验证效率低下。为了避免上述情况，需要一种更加紧凑且高效的数据平面模型表达，从而提高整体验证效率。

\subsection{数据平面的逆向模型表示}


\begin{definition}
  \textbf{转发等价类}。对于一个包头空间$H$，如果对任一设备$d \in D$，$\forall h_i,h_j \in H: F(d, h_i) = F(d, h_j)$，则$H$构成一个转发等价类。
\end{definition}

\begin{theorem}
  \label{thm:fec}
  给定一个数据平面模型$M$，如果$\forall H_i,H_j \in \Sigma: H_i \cap H_j = \emptyset$，则$\forall H \in \Sigma$，$H$构成一个转发等价类。
\end{theorem}

\begin{proof}
  采用反证法证明定理~\ref{thm:fec}，如果$H \in \Sigma$不构成转发等价类，则$\exists d \in D$，使得$\exists h_i,h_j \in H: \mathcal{F}(d, h_i) \neq \mathcal{F}(d, h_j)$，那么$\exists e_i,e_j \in A_d^{out}: h_i \in \bigcup_{H \in \delta(e_i)}H, h_j \in \bigcup_{H \in \delta(e_j)}H, e_i \neq e_j$。然而，$\Sigma$是$\mathbb{H}$的一个划分，且$h_i$和$h_j$属于同一个划分，意味着如果$h_i \in \bigcup_{H \in \delta(e_i)}H$，则$h_j \in \bigcup_{H \in \delta(e_i)}H$，说明$\mathcal{F}(d, h_i) = \mathcal{F}(d, h_j)$，与前提条件冲突。
\end{proof}

基于\cref{thm:fec}，容易证明已有工作如Veriflow~\cite{khurshid2012veriflow}和DeltaNet~\cite{horn2017deltanet}所构建的数据平面模型为上述的模型的特例（由于其划分的包头空间互不重叠）。然而，它们利用区间形式表示一个等价类，这种方式在存在非前缀匹配的情况下会导致产生大量的转发等价类。为了解决上述问题，需要有更高效的方式表达包头空间，实现转发等价类的聚合，从而减少转发等价类的数量，基于原子谓词（Atomic predicates，AP）的数据平面模型将包头空间抽象为谓词形式，提供了更一般化的包头空间表达和操作。

\begin{definition}
  \textbf{数据包头的谓词形式}：令$\{x_1,...x_n\}$为一个布尔变量集合，对于一个数据包头$h=\{b_1,...,b_n\}$，可以将其表示为一个布尔逻辑表达式$p_h = c_1 \wedge c_2 ... \wedge c_n$ （简写为$c_1c_2...c_n$），其中：
\end{definition}
\begin{equation}
  c_i = \begin{cases}
    x_i & b_i = 1 \\
    \bar{x_i} & b_i = 0
  \end{cases}
\end{equation}
例如，数据包头 1010 表示为布尔逻辑表达式为$x_1\bar{x_2}x_3\bar{x_4}$。

% 一个数据包头$h$可以根据数据包转发协议进行分组，如源IP地址，目的IP地址等。则$h=\{field_1,...field_n\}$，其中$field_i$表示数据包头的第$i$组布尔变量。

\begin{definition}
  \label{def:hspred}
  \textbf{包头空间的谓词形式}：包头空间$H=\{h_1,...h_k\}$的布尔逻辑表达式为其所包含的所有数据包头的布尔表达式的析取，$p_H = \vee_{i=1}^k p_{h_i}$。
\end{definition}

例如，数据包头 1010 和 1011 构成的包头空间布尔逻辑表达式为$x_1\bar{x_2}x_3\bar{x_4} \vee x_1\bar{x_2}x_3x_4 = x_1\bar{x_2}x_3$。给定一个数据包头，可以很容易根据该数据包头生成布尔表达式的变量值，进而验证该数据包头是否满足一个布尔表达式，所以也将上述布尔表达式称为\textbf{谓词} (predicates)，对于一个谓词$p$，用$p(h)$表示作为一个指示函数（indicator function），其值表示$h$对应的变量取值是否能够使$p$为True。所以，一个predicate $p$表示了一个包头空间$HS(p) = \{h | p(h) = True, \forall h \in \mathbb{H}\}$。

另外，FIB规则的match域往往表达为一个带有通配符（wildcard）的包头空间（如IP前缀），可以很容易表达为谓词形式，令$\{b_1,...,b_n\}$为带通配符的包头空间，$b_i \in \{0,1,\text{x}\}$，该包头空间可以表示为谓词$c_1 \wedge c_2 ... \wedge c_n$，其中：
\begin{equation}
  c_i = \begin{cases}
    x_i & b_i = 1 \\
    \bar{x_i} & b_i = 0 \\
    True & b_i = \text{x}
  \end{cases}
\end{equation}
例如，数据包头 1*0* 表示为布尔逻辑表达式为$x_1\bar{x_3}$。本文用$pred(m)$表示一个match域$m$对应的谓词。

\textbf{包头空间和谓词的等价性}。表~\ref{tab:hs-pred-op} 列出了主要的包头空间操作及其等价的谓词操作和证明过程，其中$H_i,H_j \in 2^\mathbb{H}$为两个包头空间，其对应的谓词分别为$p_i$和$p_j$。由于谓词和包头空间的等价性，在上下文清晰的情况下，\textbf{之后的内容将不再区分包头空间和谓词}，使用谓词及其相关符号来表示包头空间及其操作。

\begin{table}[]
  \center
  \caption{包头空间操作及其等价的谓词操作}
  \label{tab:hs-pred-op}
  % \resizebox{\linewidth}{!}{
  \begin{tabular}{|c|c|c|c|c|c|c|}
    \hline
    \emph{包头空间操作}
    & \emph{等价谓词操作}
    & \emph{证明}
    \\\hline
    $H_i \cup H_j$ & $p_i \vee p_j$ & $HS(p_i \vee p_j) = HS(p_i) \cup HS(p_j) = H_i \cup H_j$
    \\\hline
    $H_i \cap H_j$ & $p_i \wedge p_j$ & $HS(p_i \wedge p_j) = HS(p_i) \cap HS(p_j) = H_i \cap H_j$
    \\\hline
    $H_i - H_j$ & $p_i \wedge \neg p_i$ & \makecell[c]{$HS(p_i \wedge \neg p_i) = HS(p_i) \cap HS(\neg p_j)$\\ $= HS(p_i) \cap (\mathbb{H} - HS(p_j)) = H_i - (H_i \cap H_j) = H_i - H_j$}
    \\\hline
    $\mathbb{H} - H_i$ & $\neg p_i$ & $HS(\neg p_i) = \mathbb{H} - HS(p_i) = \mathbb{H} - H_i$
    \\\hline
    $H_i = \emptyset$ & $p_i = False$ & \multirow{3}{*}{定义~\ref{def:hspred}即可证明}
    \\\cline{1-2}
    $H_i = \mathbb{H}$ & $p_i = True$ & 
    \\\cline{1-2}
    $H_i =(\neq) H_j$ & $p_i =(\neq) p_j$ & 
    \\\hline
    $H_i \subseteq H_j$ & $p_i \wedge p_j = p_i$ & \makecell[c]{$H_i \subseteq H_j \Leftrightarrow HS(p_i \wedge p_j) = H_i \cap H_j = H_i \Leftrightarrow p_i \wedge p_j = p_i$}
    \\\hline
  \end{tabular}
  % }
\end{table}


有了数据平面模型正确性定义，还需要尽可能实现最优的数据平面模型，消除冗余的数据，从而使验证过程更加高效，定义最优的数据平面模型如下。
\begin{definition}
  \textbf{数据平面模型的最优性}。给定一个数据平面$DP$以及基于其构建的基于转发等价类数据平面模型$M$，如果$\nexists M'(V,A,\Sigma', \delta') \sim DP: |\Sigma'| < |\Sigma|$，且$M'$为基于等价类的数据平面模型，则称$M$是$DP$的最优数据平面模型。
\end{definition}

为了实现最优数据平面模型，需要对$\Sigma$的划分进一步优化。基于原子谓词（Atomic predicates）的数据平面模型能够很好的解决该问题。

\begin{definition}
  \textbf{原子谓词（Atomic Predicates）}。令$\mathcal{P}$为一个谓词集合，其原子谓词$\{p_1,...,p_k\}$满足以下条件：
\end{definition}
\begin{enumerate}
  \item $\forall i \in \{1,...,k\}: p_i \neq False$;
  \item $\bigvee_{i=1}^k p_i = True$;
  \item $\forall i \neq j \in \{1,...,k\}: p_i \wedge p_j = False$;
  \item 每个谓词$p \in \mathcal{P}$可以表达为若干个原子谓词的析取，即$p = \bigvee_{i \in S(P)}p_i$，其中$S(P) \subseteq \{1,...,k\}$；
  \item $k$为满足上述条件的最小值。
\end{enumerate}

构建基于原子谓词的数据平面模型需要经历两个过程，首先需要将每个设备的FIB转换成谓词形式，从而得到初始谓词集合，然后对谓词集合求原子谓词。AP的计算过程本质上是对原始谓词进行划分，比如APV~\cite{yang2016realtime}的AP计算过程以及APKeep~\cite{zhang2020apkeep}的split算法。

由于规则优先级的存在，具有相同语义的两个FIB可能会有不同的结构。
\begin{definition}
  FIB的等价性。对于两个FIB $R_1$和$R_2$，如果二者具有相同的转发语义，即$\forall h \in \mathbb{H}: F_1(h)=F_2(h)$，则二者是等价的，记为$R_1 \sim R_2$.
\end{definition}

\begin{definition}
  \label{def:fib-pred}
  FIB的谓词形式。给定任意一个FIB $R$，其谓词形式为一个二元组集合$P_R=\{\langle p_1,a_1 \rangle,...,\langle p_n,a_n \rangle\}$，其中$p_i$为一个谓词，$a_i$为对应的动作。
  FIB的谓词形式具有如下特性：
\end{definition}
\begin{enumerate}
  \item $p_i \wedge p_j = False$ iff $i \neq j$;
  \item $\bigvee_{i=1}^n p_i = True$;
  \item $a_i \neq a_j$ iff $i \neq j$;
\end{enumerate}

FIB的谓词形式计算过程如下，给定一个FIB $R$，令$\langle p_i, a_i\rangle$为$P_R$的元素，其中，$a_i \in \{a_r|r \in R\}$，$p_i=\vee_{r \in R|_{action=a_i}} hit_r$，此处$hit_r$表示规则$r$能匹配的包头空间的谓词形式，令$R|_{pri > r.pri}$表示所有优先级高于$r$的规则，则$hit_r = pred(r.match)\wedge \neg(\vee_{r' \in R_{pri > r.pri}} pred(r'.match))$。

\begin{theorem}
\label{the:predFIBequ}
  对于两个FIB $R_1$和$R_2$，令$P_1$和$P_2$分别为其谓词形式，如果$R_1 \sim  R_2$，则$P_1 = P_2$。
\end{theorem}
\begin{proof}
  若$R_1 \sim  R_2$且$P_1 \neq P_2$，则存在包头$h$，使得$\exists \langle p_i,a_i \rangle \in P_1: p_i \wedge h \neq False$， $\exists \langle p_j,a_j \rangle \in P_2: p_j \wedge h \neq False$，且$a_i \neq a_j$，那么意味着$h$在$P_1$和$P_2$中具有不同转发行为，而根据\cref{def:fib-pred}给出的FIB谓词形式计算过程，$\exists r_i \in R_1, r_j\in R_2: h \in hit_{r_i} \wedge h \in hit_{r_j} \wedge r_i.action \neq r_j.action$，则$R_1$和$R_2$具有不同语义，与前提矛盾。
\end{proof}

\begin{theorem}
  FIB谓词形式的唯一性。对于具有相同语义的FIB族$\mathbb{T}=\{T_1,...,T_n\}$，$T_1 \sim T_2 \sim ... \sim T_n$，该FIB族的谓词形式是唯一的。
\end{theorem}
\begin{proof}
  根据定理~\ref{the:predFIBequ}，$\mathcal{T}_1 = \mathcal{T}_2=...=\mathcal{T}_n$，则$\mathbb{T}$中所有元素对应同一个谓词形式。
\end{proof}

\textbf{逆向模型（等价类表示）。}
网络数据平面的等价类表示记为$M = \{(p^j, \vec{y}^j)\}_j$，其中$(p^j, \vec{y}^j)$表示$M$中的第$j$个元素。对于每个$j$，$p^j$是一个谓词，$\vec{y}^j$是一个$N$维动作向量，其中$y^j_i$指定第$i$个设备上的动作。在有效的等价类表示$M$中，条目满足以下条件：1）\emph{唯一性}：$\forall j \neq j^\prime$，$\vec{y}^j \neq \vec{y}^{j^\prime}$；2）\emph{互斥性}：$\forall j \neq j^\prime$，$\forall h$，$p^j(h) \wedge p^{j^\prime}(h) = 0$；以及3）\emph{互补性}：$\forall h$，$\exists j$，$p^j(h) = 1$。


虽然如HSA~\cite{kazemian2012header}等工作使用前向模型（基于规则的表示）能够将包头空间映射到action集合，较为容易实现任意包头的验证，但难以确定具有特定action的包头空间是什么，而逆向模型（等价类表示）则提供了一种高效的数据结构，使得在给定转发行为$\vec{y}^{j}$的情况下，也可以找到对应的数据包头空间$p^{j}$，模型结构能够给出双向视角，从而使得数据平面验证器能够检查是否存在违规的路径$\vec{y}^{j}$。因此，Flash采用逆模型作为其数据平面模型结构，而数据平面模型构建的目标是将前向模型$\mathcal{R}$转换为逆向模型$M$，且$\mathcal{R}$与$M$等价，记为$\mathcal{R} \sim M$，其定义为，当且仅当$\forall h$，$\vec{b}_\mathcal{R}(h) = \vec{b}_M(h)$。

\cref{fig:model-fimt-example} 左下角标记为$M$的表是$\mathcal{R}$的逆向模型。可以观察到网络具有两种行为：$(A, S_1, S_1)$对应于$p_1 \lor p_2$的数据包头，以及$(S_3, S_3, GW)$对应其余的数据包头。Flash构建一个图数据结构来表示这些向量，并运行图算法来检查图上的属性（例如可达性和无环）。

% Flash基于原子谓词~\cite{yang2016realtime}的等价类结构表示数据平面模型，由于原子谓词所表达的数据平面模型为双射结构，即每个原子谓词表示的包头空间与action集合一一对应，可以很容易通过action来找到对应的包头空间，这样的形式与如HSA~\cite{kazemian2012header}所使用的结构恰好相反，本文将基于原子谓词的等价类结构其命名为数据平面的逆模型结构。
% 网络数据平面配置$C$包含$N$个设备（路由器或交换机），可以有两种不同的表示方式来定义任意数据包头$h$的相同转发行为：基于规则的表示（Forward model）和等价类表示（Inverse model）。


\subsection{快速逆模型变换}
为了实现的$\mathcal{R}$到$M$的变换，关键在于如何避免因$\mathcal{R}$中规则的相关性导致错误的聚合结果，Flash通过计算原子覆写（Atomic overwrites）来解决该问题，具体而言，原子覆写是由一个二元组集合组成，表示为$\{\langle p_1, a_1 \rangle,...,\langle p_N, a_N \rangle\}$。其中，$p_i$是一个谓词，$a_i$是一个由转发规则定义的动作。其语义是当网络设备接收到符合谓词$p_i$的数据包时，将使用动作$a_i$对其进行处理，并且对于任意的谓词$p_i$和$p_j$，满足$p_i \wedge p_j = False$，即所有谓词之间是互斥的。由于这种互斥关系，本文将其称为原子覆写。由于原子覆写的谓词互斥，这种无关性使得Flash可以对原子覆写进行顺序无关的聚合，从而得到最终对数据平面模型的更新。

\cref{fig:model-fimt-example}给出了Flash实现快速逆模型变换的示例，在数据平面发生更新，如规则插入、删除或修改时，基于规则的表示（前向模型）从初始状态$\mathcal{R}$转变为最终状态$\mathcal{R}^\prime$。相应地，等价类模型（逆向模型）必须从初始状态$M$转变为最终状态$M^\prime$，其中$\mathcal{R}^\prime \sim M^\prime$。\cref{fig:model-fimt-example}的右侧显示了当在三个交换机中插入规则以处理HTTP数据包时，数据平面更新后对应的数据平面模型示例。该过程是全局原子谓词计算过程APV~\cite{yang2016realtime}和APKeep~\cite{zhang2020apkeep}的一般化：全局原子谓词解决了没有初始规则的特殊情况，即$\mathcal{R} = (\emptyset, \dots, \emptyset)$，而APKeep的工作则解决了每次更新只有一条规则的特殊情况。

Flash实现数据平面更新批处理的核心在于快速计算原子覆写（Atomic overwrites），Flash基于MapReduce框架实现该过程，本文将其称为FIMT（Fast Inverse Model Transformation）。具体而言，FIMT包含一个Map函数和两个Reduce函数，称为MR2算法。以\cref{fig:model-fimt-example}所示为例，Map函数分别对每个设备上的更新计算原子覆写（Atomic overwrites），然后，Flash对Map函数生成的结果按照action进行Reduce操作 (Reduce I)，对具有相同action的原子覆写合并（谓词进行析取操作），得到各个设备上以action为主键的原子覆写。之后，Flash对Reduce I生成的所有结果进行第二次Reduce操作(Reduce II)，将具有相同谓词的条目进行合并，action则直接进行集合并操作，得到最终的数据平面模型更新$\Delta M$。最后，Flash将$\Delta M$于原始数据平面模型进行乘积操作（与APV~\cite{yang2016realtime}计算AP类似），从而得到最终的数据平面模型。

算法~\ref{alg:compute-local-model} 中的\textbf{ComputeAO}函数给出了并行化的原子覆写计算过程，该函数输入为删除/新增的数据平面规则$\Delta R^-/\Delta R^+$和更新后的数据平面规则$R$，输出为对应设备的原子覆写。该算法首先找到受影响的规则$R_{aff}$（L3），\textbf{FindAffected}函数并行地计算每条更新造成的受影响规则（L14-19），其中\textbf{OverlapRulesLP}函数找出$R$中与$r$的match域相交，且优先级低于$r$的所有规则（L17），同时，对于新增的规则，将其加入到受影响规则集合(L4)。然后，对于每个受影响规则，并行地计算这些规则的有效匹配包头空间（hit），函数\textbf{OverlapRulesHP}用于计算$R$中优先级高于$r$且与$r$的match域相交的所有规则（L6），并计算已经这些规则处理的包头空间$fwd$（L7-8），如果更新的有效匹配包头空间与原来的hit不同，则将其插入到原子覆写集合，并更新该规则的有效匹配空间（L10-12）。对于Reduce I和Reduce II函数，Flash采用并行方式实现并行聚合，具体将在\cref{sec:model-solution-par}介绍。

\begin{algorithm}[h]
  \caption{ComputeAO: 计算原子覆写}
  \label{alg:compute-local-model}
  \KwIn{$R$: 更新后的数据平面规则; $\Delta R^-$: 删除的数据平面转发规则; $\Delta R^+$: 新增的数据平面转发规则}
  \KwOut{$O$: 原子覆写}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKwProg{Pf}{parallelFor}{ do}{}{}
  \SetKwFunction{Pr}{ParallelReduce}

  \Fn{$\FuncSty{ComputeAO}(\Delta R^-, \Delta R^+, R)$}{
    $O \gets \{\}$\;
    $R_{aff} \gets \FuncSty{FindAffected}(\Delta R^- \cup \Delta R^+, R)$\;
    $R_{aff} \gets R_{aff} \cup \Delta R^+$\;
    \Pf{$r \in R_{aff}$}{
      $R' \gets \FuncSty{OverlapRulesHP}(r, R)$\;
      $P \gets \bigcup_{r' \in R'}r'.hit$\;
      $fwd \gets $\Pr{$P, False, \vee$}\;
      $hit \gets r.hit \wedge \neg fwd$\;
      \If{$hit \neq r.hit$}{
        $O \gets O \cup \{hit, r.action\}$\;
        $r.hit \gets hit$\;
      }
    }
    \Return{$O$}\;
  }
  % \ForEach{$r \in \Delta R^-$}{
  %   $R' \gets OverlapRulesLP(r, R)$\;
  %   $R' \gets SortByPriority(R')$\;
  %   $remain \gets r.hit$\;
  %   \ForEach{$r' \in R'$}{
  %     $p \gets remain \wedge r'.hit$\;
  %     $r'.hit \gets r'.hit \vee p$\;
  %     \If{$p \neq False$ and $r.action \neq r'.action$}{
  %       $O \gets O \cup \{p, r'.action\}$\;
  %     }
  %     $remain \gets remain \wedge \neg p$\;
  %   }
  % }

  % \ForEach{$r \in \Delta R^+$}{
  %   $R' \gets OverlapRules(r, R \cup \Delta R)$\;
  %   $P \gets \{\}$\;
  %   \Pf{$r' \in R'$}{
  %     $P \gets P \cup \{r'.hit\}$\;
  %   }
  %   $fwd \gets $\Pr{$P, False, \vee$}\;
  %   $r.hit \gets r.hit \wedge \neg fwd$\;
    
  %   $O \gets O \cup \{r.hit, r.action\}$\;

  %   % $hit \gets H_r \wedge \not fwd$\;
  %   % $p_{(d, r.nh)} \gets p_{(d, r.nh)} \vee hit$\;
  %   % $fwd \gets fwd \vee H_r$\;
  % }
  
  \Fn{\FuncSty{FindAffected}{($\Delta R, R$)}}{
    $S \gets set()$\;
    \Pf{$r \in \Delta R$}{
      $S \gets S \cup \FuncSty{OverlapRulesLP}(r, R)$\;
    }
    \Return{$S$}
  }
\end{algorithm}


\section{基于并行流水线的数据平面模型构建方法}
\label{sec:model-solution-par}
为了解决挑战C2（数据平面更新并行处理的顺序随机性），且不丢失并行特性，流水线结构是一种能够保证执行顺序且不失并行特性的方法，所以本文提出了\textbf{S2:基于并行流水线的数据平面模型构建方法}，在这种方法中，数据平面模型的构建过程被划分为多个阶段(Stage)，并在每个阶段中使用并行计算来加速模型构建过程。流水线结构能够充分利用服务器多核并行优势，并行地对数据平面更新进行处理，从而应对大规模数据平面更新带来的效率问题。


在本文作者前期所发表的论文Flash~\cite{guo2022flash}中主要实现了数据平面更新的批处理过程。然而，对于每个更新块，前期研究尚未实现并行化和流水线化处理，这意味着每个更新块必须等待上一个更新块处理完毕才能进行处理。此外，尽管更新块的处理采用了MapReduce架构，但由于当前主流的BDD库(如JDD~\cite{vahidi2023bdd})不是线程安全的，因此每个更新块的处理仍以单线程方式实现，导致Flash无法充分利用服务器资源进而提高验证系统的伸缩性。本文在前期研究的基础上进一步扩展了Flash的并行特性，以提高验证系统的伸缩性。

\begin{figure}[]
  \centering
  \includegraphics[width=\textwidth]{figures/model/parallel.pdf}
  \caption{并行数据平面模型构建示例}
  \label{fig:parallel-example}
\end{figure}

图~\ref{fig:parallel-example} 中的示例描述了通过并行批处理方式实现数据平面模型构建过程。其中包含两个网络设备$S_1$和$S_2$，$S_1$与分配有IP前缀10.0.0.0/16的网络$A$连接，$S_2$与网关GW连接，$\mathcal{R}$和$M$分别为原始数据平面配置和原始数据平面模型，$\mathcal{R}'$和$M'$分别为系统收到数据平面配置更新$\Delta R$后的数据平面配置和数据平面模型，$\Delta R$中的规则添加了对IP前缀10.0.0.0/24和10.0.0.0/8的路由。图~\ref{fig:parallel-example} 中绿色箭头表示并行执行，蓝色箭头表示并行聚合，系统收到数据平面配置批量更新$\Delta R$后进行以下并行处理过程：

\begin{enumerate}
  \item 并行数据平面配置更新标准化：对$\Delta R$中的每条规则，并行地将其match域转换为谓词，生成谓词形式的数据平面更新$\Delta R'$，每个谓词对应的包头空间在图~\ref{fig:parallel-example} 下方列出。该过程可进行并行的原因在于每条规则的谓词形式只依赖于规则本身match域的值。
  \item 并行原子覆写计算：对$\Delta R'$中的每条规则，并行地计算其原子覆写，生成$O'$。该过程可进行并行的原因有两个，首先，对于每个更新规则，其造成的原子覆写只与相应设备的FIB有关，其次，计算原子覆写的过程只和与该规则match域有重叠的规则有关，并不依赖于其他规则生成的原子覆写结果。
  \item 并行数据平面模型更新聚合：对$O'$中的所有规则首先对action域相同的元素进行聚合，然后对谓词域相同的元素进行聚合，生成数据平面模型更新$\Delta M$。该过程可以进行并行聚合的原因在于上述两种操作均满足交换律。
  \item 并行数据平面模型更新：对$\Delta M$和$M$中的元素进行并行乘法操作，并进一步对结果按照action进行并行聚合得到$M'$。该过程可以并行的原因在于对每个元素$(i, j) \in \Delta M \times M$计算原子谓词时只依赖与$i$和$j$，且聚合过程为谓词合并($\vee$)过程，满足交换律。
\end{enumerate}

% 数据平面模型构建包括初始化构建，以及数据平面更新处理。本文统称位数据平面模型构建。

\subsection{并行数据平面更新标准化}
数据平面更新标准化过程主要将输入验证系统的数据平面规则更新转化为谓词形式，该过程在所有的基于原子谓词的验证系统中都是必须的，已有工作如Flash~\cite{guo2022flash}，APV~\cite{yang2016realtime}，APT~\cite{yang2017scalable}，APKeep~\cite{zhang2020apkeep}和DNA~\cite{zhang2022differential}等均采用串行方式处理。
% ，其复杂度为$O(K\times N)$，其中$K$为数据平面更新数量，$N$为包头长度。
代码~\ref{alg:normalize} 实现了并行化的数据平面更新标准化过程，其中关键字\textbf{parallelFor}表示并行处理，函数\textbf{ParallelReduce}($list, init, op$)表示并行对一个集合$list$进行$op$类型的聚合（Reduce）操作，初始值为$init$。在该算法中，每个数据平面规则可以并行地进行标准化处理（L1），对于每个规则，首先并行地获得规则match域所对应的布尔变量（L2-8），最后通过并行方式对所有的布尔变量进行合并，并作为该规则的初始化可匹配包头空间（L9）。
% ，算法复杂度为$O(\log K \times \log N)$。
\begin{algorithm}[h]
  \caption{Normalize: 数据平面更新标准化}
  \label{alg:normalize}
  \KwIn{$\Delta R$: 数据平面规则更新; $N$: 数据包头长度; $X=\{x_1,...,x_N\}$: 布尔变量集合}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKwProg{Pf}{parallelFor}{ do}{}{}
  \SetKwFunction{Pr}{ParallelReduce}
  \Fn{\FuncSty{Normalize}($\Delta R, N, X$)}{
    \Pf{$r \in \Delta R$}{
      $vars \gets \{\}$\;
      \Pf{$i \in [0, N - 1]$}{
        $b \gets $ $r.match$中第$i$位的比特值\;
        \If{$b = 1$}{
          $vars \gets vars \cup \{x_i\}$\;
        }
        \If{$b = 0$}{
          $vars \gets vars \cup \{\neg x_i\}$\;
        }
      }
      $r.hit \gets $\Pr{$vars, True, \wedge$}\;
    }
  }
\end{algorithm}

\subsection{并行原子覆写计算}
对数据平面规则进行标准化后，针对每个更新的设备，FIMT计算其数据平面的原子覆写（Atomic overwrites）。\cref{alg:ParComputeAO}所示为并行原子覆写计算过程，对于每个设备$i$的更新并行执行以下过程：首先根据其类型（如添加、删除规则）对规则进行分组（L4），然后将规则更新应用到设备原始的规则集合（L5），再通过\cref{alg:compute-local-model}计算各个设备的原子覆写，合并到最后结果集并返回（L5-7）。



\begin{algorithm}[h]
  \caption{ParComputeAO: 并行原子覆写计算}
  \label{alg:ParComputeAO}
  \KwIn{$\{\Delta R_1',...,\Delta R_N'\}$: 每个设备数据平面更新规则}
  \KwOut{$\{O_1',...,O_N'\}$: 原子覆写}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKwProg{Pf}{parallelFor}{ do}{}{}
  \Fn{$\FuncSty{ParComputeAO}(\{\Delta R_1',...,\Delta R_N'\})$}{
    $O' \gets \{\}$\;
    % $group \gets $ 根据action对$O$进行分组\;
    \Pf{$i \in [1,...,N]$}{
      $\{\Delta R^-,\Delta R^+\} \gets \FuncSty{GroupByType}(\Delta R_i')$\;
      $R_i \gets R_i \cup R^+ / R^-$\;
      $O_i' \gets \FuncSty{ComputeAO}(\Delta R^-,\Delta R^+, R_i)$\;
      $O' \gets O' \cup \{O_i'\}$\;
    }
    \Return{$O'$}\;
  }
\end{algorithm}

\subsection{并行数据平面更新聚合}
由于原子覆写的互斥特性，可以对其进行聚合操作，以消除冗余操作从而进一步提高数据平面模型更新效率。首先，同一设备的原子覆写可以根据action进行聚合，算法~\ref{alg:reduce1} 给出了具体的聚合过程，首先对$O$根据action进行分组（L3），其中$group$为一个key-value结构，key为action，value为具有相同action的原子覆写集合。对于$group$中的每个元素，并行地将具有相同action的原子覆写的谓词合并（L4-7），最后返回聚合后的原子覆写（L8）。

然后，对所有设备聚合后的原子覆写进行进一步进行全局聚合，从而得到数据平面模型更新$\Delta M$。算法~\ref{alg:reduce2} 给出了并行化的全局聚合过程，首先根据谓词对所有的原子覆写进行分组（L3），$group$的key为谓词，value为具有相同谓词的原子覆写集合。对于$group$中的每个元素，并行地将具有相同谓词的原子覆写的action合并（L4-6），最后返回聚合后的数据平面模型更新（L7）。

\begin{algorithm}[h]
  \caption{Reduce I: 按照action聚合}
  \label{alg:reduce1}
  \KwIn{$O'$: 原子覆写}
  \KwOut{$O$: 聚合后的原子覆写}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKwProg{Pf}{parallelFor}{ do}{}{}
  \Fn{$\FuncSty{ReduceI}(O')$}{
    $O \gets \{\}$\;
    $group \gets $ 根据action对$O$进行分组\;
    \Pf{$(action, g) \in group$}{
      $P \gets \bigcup_{o \in g}o.pred$\;
      $p \gets \Pr(P, False, \vee)$\;
      $O \gets O \cup \{p, action\}$\;
    }
    \Return{$O$}\;
  }
\end{algorithm}

\begin{algorithm}[h]
  \caption{Reduce II: 按照谓词聚合}
  \label{alg:reduce2}
  \KwIn{$O$: 原子覆写}
  \KwOut{$\Delta M$: 数据平面模型更新}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKwProg{Pf}{parallelFor}{ do}{}{}
  \Fn{$\FuncSty{ReduceII}(O)$}{
    $\Delta M \gets \{\}$\;
    $group \gets $ 根据谓词对$O$进行分组\;
    \Pf{$(p, g) \in group$}{
      $Y \gets \bigcup_{o \in g}o.action$\;
      $\Delta M \gets \Delta M \cup \{p, Y\}$\;
    }
    \Return{$\Delta M$}\;
  }
\end{algorithm}

\subsection{并行数据平面模型更新}
算法~\ref{alg:model-update} 给出了并行化的数据平面模型更新过程，函数\textbf{ModelUpdate}输入数据平面更新$\Delta M$以及原始数据平面模型$M$，对于$M$中的每个元素，并行地对谓词进行划分（L2-12），对$\Delta M$中的每个元素，并行地计算其与原始数据平面模型谓词的交集$\eta$，如果交集非空且action数组不同，则将原始数据平面谓词进行划分（L5-8），同时用$\Gamma$记录已经划分的谓词(L7)。然后，计算原始数据平面模型元素谓词的剩余部分（L9-10），并用剩余部分替换原始数据平面模型中的元素（L11-12）。最后，对数据平面模型中具有相同action数组的谓词进行合并（L13），具体实现在函数\textbf{Merge}(L14-20)，该函数首先根据action对$M$进行分组（L15），对于$group$中的每个元素，并行地将具有相同action的谓词合并（L17-18），并替换相应的数据平面模型元素（L19-20）。

\begin{algorithm}[h]
  \caption{ModelUpdate: 数据平面模型更新}
  \label{alg:model-update}
  \KwIn{$M$: 原始数据平面模型}
  \KwIn{$\Delta M$: 数据平面模型更新}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKwProg{Pf}{parallelFor}{ do}{}{}
  \Fn{$\FuncSty{ModelUpdate}(\Delta M, M)$}{
    \Pf{$(p, Y) \in M$}{
      $\Gamma \gets \{\}$\;
      \Pf{$(p', Y') \in \Delta M$}{
        $\eta \gets p \wedge p'$\;
        \If{$\eta \neq False$ and $Y \neq Y'$}{
          $\Gamma \gets \Gamma \cup \{\eta\}$\;
          $M \gets M \cup \{(\eta, Y')\}$\;
        }
      }
      $\gamma \gets \Pr(\Gamma, False, \vee)$\;
      $\eta' \gets p \wedge \neg \gamma$\;
      $M \gets M / \{(p, Y)\}$\;
      $M \gets M \cup \{(\eta', Y)\}$\;
    }
    $\FuncSty{Merge}(M)$\;
  }
  \Fn{$\FuncSty{Merge}(M)$}{
    $group \gets $ 根据action对$M$分组\;
    \Pf{$(Y, g) \in group$}{
      $P \gets \bigcup_{m \in g}m.pred$\;
      $p \gets \FuncSty{ParallelReduce}(P, False, \vee)$\;
      $M \gets M / g$\;
      $M \gets M \cup \{p, Y\}$\;
    }
  }
\end{algorithm}

% \subsection{并行化数据平面模型构建分析}
% % 本文用一个DAG图来描述数据平面模型构建过程，并分析其中可并行部分，其中具有依赖关系的过程被设计为流水线方式执行，否则可以并行执行。

% 图~\ref{fig:pipeline} 所示为Flash所采用的流水线结构，该流水线结构包含四个stage，每个stage之间通过队列进行通信。同时，stage中对BDD的处理采用并行结构，从而提高整体系统的吞吐量。
% \begin{itemize}
%   \item 数据平面更新标准化（Normalizer）
%   \item 数据平面模型更新计算（Change expander）
%   \item 数据平面模型更新聚合（Aggregator）
%   \item 数据平面模型更新（Model updater）
% \end{itemize}

% \begin{figure}[htbp]
%   \centering
%   \includegraphics[width=\textwidth]{model/pipeline.pdf}
%   \caption{基于流水线结构的数据平面模型并行构建}
%   \label{fig:pipeline}
% \end{figure}

% 基于流水线结构的数据平面模型并行构建方法可以充分利用并行计算的优势，提高模型构建的效率和性能。它适用于大规模网络和复杂数据平面的场景，可以加速数据平面模型的生成和更新过程。

\section{面向大规模谓词操作的BDD库}
\label{sec:model-solution-bdd}



为了解决挑战C3（BDD 并发操作的不一致性），本文提出了\textbf{S3: 面向大规模谓词操作的BDD库}。在数据平面模型的并行构建过程中，多个线程会同时进行BDD操作，因此需要保证BDD的操作的线程安全性。然而，简单的使用全局mutex锁来限制同一时间只有一个BDD操作会导致效率和资源利用率低下。因此，需要设计一种线程安全且支持BDD并行操作的机制。


具体而言，数据平面验证系统的可伸缩性受限于BDD操作的可伸缩性，原因有两个：1) \textbf{BDD操作占据了大部分验证时间}。在相关研究如Flash~\cite{guo2022flash}显示，BDD操作占据了大部分验证时间（即BDD操作数量达到$O(10^9)$的数量级，并占据了总体时间的99\%以上）。2) \textbf{由于底层BDD包缺乏并行支持，许多并行化的过程无法实现}。以Flash~\cite{guo2022flash}为例，尽管其采用了Map-Reduce设计，但实际实现中由于底层BDD库缺乏线程安全操作，导致map函数被顺序执行。此外，与Coral~\cite{xiang2022network}等系统的开发人员讨论后发现，他们也面临着同样的问题。

值得注意的是，诸如包头空间划区~\cite{zeng2014libra}和拓扑划区~\cite{jayaraman2019validating,xiang2022network}等技术与本文的特定目标是正交的。它们可以与本文方法共同使用来提高整体的数据平面模型构建吞吐量和伸缩性。比如，根据包头空间可以将数据平面更新分割成更小的部分，并将其分布在多个处理器或计算节点上，结合BDD并行基础设施，允许更好的资源利用和分布式计算，可以实现更好的并行性和伸缩性，以达到更高效的数据平面验证目的。

\subsection{BDD构建过程概述}
一个布尔表达式可以用一个完整的二叉树来表示，这个二叉树被称为二叉决策树，它是基于表达式的真值表而建立的。图~\ref{fig:bdt-example}显示了一个布尔表达式$f=x_1x_3 \vee \bar{x_1}x_2x_3$的真值表和相应的二叉决策树。二叉决策树中的每个内部节点都被标记为一个变量，并且有两个分支：low-分支（虚线）对应变量赋值为0的情况，high-分支（实线）对应变量赋值为1的情况。每个叶子节点都被标记为0或1。从根节点到叶子节点的每条路径对应于一个真值表条目，其中叶子节点的值是函数的值，路径对应于布尔变量的赋值。


\begin{figure}[htbp]
  \centering
  \includegraphics[width=0.9\textwidth]{model/bdt-example.pdf}
  \caption{布尔表达式$f=x_1x_3 \vee \bar{x_1}x_2x_3$的二叉决策图和真值表}
  \label{fig:bdt-example}
\end{figure}

二叉决策图（BDD）~\cite{akers1978binary}是二叉决策树的等价表示，具有相同的真值表。图~\ref{fig:bdd-example}展示了图~\ref{fig:bdt-example}中的布尔函数的BDD表示。给定一个变量顺序，一个布尔函数的BDD的表示是唯一的，BDD可以比其对应的真值表或二叉决策树表示更加紧凑~\cite{bryant1986graphbased}。在构建BDD的过程中，保证BDD唯一性的标准是构建所有的BDD节点必须遵循相同的变量顺序，即在任何BDD的路径上，对于任意两个变量 $x$ 和 $y$ ，如果$x$的变量顺序在$y$之前，那么在该路径上 $x$ 必须出现在 $y$ 之前~\cite{yang1997parallel}。

\begin{figure}[htbp]
  \centering
  \includegraphics[width=0.25\linewidth]{model/bdd-example.pdf}
  \caption{布尔表达式$f=x_1x_3 \vee \bar{x_1}x_2x_3$的BDD表示}
  \label{fig:bdd-example}
\end{figure}

在描述BDD的构造之前，首先介绍相关术语和符号。令$f_{\bar{x}}$ 和 $f_{x}$ 是函数 $f$ 相对于布尔变量 $x$ 的cofactor，其中 $f_{\bar{x}}$ 是将变量 $x$ 限制为 $0$ 后的函数，而 $f_{x}$ 是将变量 $x$ 限制为 $1$ 后的函数。给定一个标记为变量$x$的BDD节点$b$，令其所代表的布尔函数为$f^b$，则$b$的low-节点和high-节点分别表示$f^b_{\bar{x}}$和$f^b_x$。同时，根据Shannon expansion~\cite{shannon1949synthesis}，$f^b$可以被递归地定义为：

\begin{equation}
\label{equ:shannon-exp}
  f^b = \bar{x}f^b_{\bar{x}} \vee xf^b_x
\end{equation}

式~\ref{equ:shannon-exp}表示任意一个BDD节点的构建可以通过递归地构建其low-节点和high-节点完成。对于BDD操作，令$a$和$b$分别为两个BDD节点，$op$为一个逻辑操作符（如AND，OR，NOT），则：
\begin{equation}
\label{equ:shannon-exp-op}
\begin{aligned}
  f^a\ op\ f^b & = \tau (f^a\ \var{op}\ f^b)_\tau \vee \bar{\tau}(f^a\ \var{op}\ f^b)_{\bar{\tau}}\\
  & = \tau (f^a_\tau\ \var{op}\ f^b_\tau) \vee \bar{\tau}(f^a_{\bar{\tau}}\ \var{op}\ f^b_{\bar{\tau}})
\end{aligned}
\end{equation}

其中$\tau$是$f^a$和$f^b$中具有最优先顺序的变量，式~\ref{equ:shannon-exp-op}意味着一个BDD操作可以递归地由输入BDD的low和high-节点操作完成。

算法~\ref{alg:bdd-op} 给出了实现BDD操作的伪代码，其中函数$BDDop$为一个递归函数，第2-3行为其停止条件，当某一个输入节点为叶子节点是，返回与操作符相应的BDD节点，比如对于OR操作，如果$a=1$，则返回$b$。第4行计算输入BDD的最先顺序变量，第5-6行分别计算最终结果节点的low和high节点，其中的cofactor函数由第8-15行给出。最后，$createOrGetNode$函数创建变量为$\tau$的节点，并将其low和high节点分别指向$fLow$和$fHigh$，如果该节点已经存在，则直接返回该节点。

\begin{algorithm}[]
  \caption{BDD操作算法}
  \label{alg:bdd-op}
  \KwIn{$a,b$: BDD节点; $op$: BDD操作符}
  \SetKwProg{Fn}{Function}{:}{}
  \Fn{\FuncSty{BDDop}{$(op, a, b)$}}{
    \If{$a$ \text{is leaf} or $b$ is leaf}{
      \Return{opDefinedBDD(op, a, b)}\;
    }
    $\tau \gets \min(order(a), order(b))$\;
    $fLow = \FuncSty{BDDop}(op, \FuncSty{negCof}(a, \tau), \FuncSty{negCof}(b, \tau))$\;
    $fHigh = \FuncSty{BDDop}(op, \FuncSty{posCof}(a, \tau), \FuncSty{posCof}(b, \tau))$\;
    \Return{$\FuncSty{getOrCreateNode}(\tau, fLow, fHigh)$}\;
  }
  \Fn{\FuncSty{negCof}{$(a, \tau)$}}{
    \If{$\tau < order(a)$}{
      \Return{$a$}\;
    }
    \Return{$a.low$}\;
  }
  \Fn{\FuncSty{posCof}{$(a, \tau)$}}{
    \If{$\tau < order(a)$}{
      \Return{$a$}\;
    }
    \Return{$a.high$}\;
  }
\end{algorithm}

% 一个节点 $n$ 的可达子图定义为所有可以通过遍历一个或多个（有向）边从 $n$ 到达的节点。BDD节点被定义为BDD的内部顶点。类似于二叉决策树中的节点，每个BDD节点由一个变量和指向其两个孩子的引用组成：0分支对应于变量被赋值为 0 的情况，而l分支对应于变量被赋值为 1 的情况。

% \subsection{BDD并行处理的挑战}
% % 由于BDD构建过程为一个递归函数，
% \begin{enumerate}
%   \item BDD节点唯一性
%   \item BDD并发操作的无锁并发设计
%   \item BDD操作缓存的无锁并发设计
% \end{enumerate}

\subsection{面向大规模谓词操作的BDD库设计}
为了解决多线程并发BDD操作，本文设计实现了Nanobdd库。本节首先对Nanobdd的主要特性进行概述，在子章节中详细介绍各部分设计。具体而言，Nanobdd针对大规模数据平面验证实现了以下设计：

\begin{enumerate}
  \item \textbf{可重新调度的线程池}。为了消除线程创建和销毁的开销，Nanobdd 采用了线程池来执行BDD操作。此外，每个线程都是可重新调度的，这意味着当一个线程被阻塞时，例如等待另一个线程完成，它可以自动重新调度以执行另一个任务。这种设计有效地解决了系统中的死锁问题。这样的线程池设计具有多个优势。首先，线程池可以重复使用现有的线程，避免了频繁创建和销毁线程的开销，提高了系统的性能。其次，当一个线程被阻塞时，线程池可以将其他可用的线程调度到执行任务，避免了线程资源的浪费，提高了系统的并发性能。最重要的是，可重新调度的线程池能够有效地处理潜在的死锁情况。当一个线程需要等待另一个线程的结果时，如果后者发生死锁，可重新调度的线程池可以将等待中的线程重新分配到其他任务，避免了整个系统的死锁。通过使用可重新调度的线程池，实现了高效的并发执行和死锁的自动处理，提高了系统的性能和可靠性。这对于实现可伸缩的数据平面验证系统至关重要，特别是在面对大规模网络和复杂验证任务时。
  \item \textbf{无锁节点表和缓存}。为了实现无锁的BDD节点表和缓存，Nanobdd利用硬件提供的比较并交换（Compare-and-Swap，CAS）\cite{guerraoui2020efficient}操作，现有的BDD库\cite{tomvandijk2017sylvan,capogrosso2023hermesbdd}也有类似的设计。与其他方法不同，Nanobdd 使用动态链表来索引BDD节点，确保节点表在硬件内存完全用尽之前不会满。这消除了实时验证过程中出现意外垃圾回收的问题。通过利用硬件提供的CAS操作，Nanobdd 实现了无锁的节点表和缓存。CAS操作允许原子性地检查并更新共享数据，避免了传统的锁机制的开销和竞争。通过使用动态链表索引节点，Nanobdd 确保了节点表的可伸缩性和内存利用率。这样一来，Nanobdd 能够更有效地管理BDD节点，并且不会出现意外的垃圾回收，从而提高了验证性能和效率。与现有的BDD库相比，Nanobdd 的无锁节点表和缓存设计具有更高的并发性能和内存利用率。这对于实现可伸缩的数据平面验证系统至关重要，尤其是在处理大规模网络和复杂验证任务时。
  \item \textbf{无中断执行(RtC: Run-to-Completion)}。在并行计算中，Nanobdd 采用了无中断执行（Run-to-Completion）的方法，即每个BDD操作在执行过程中不会中断，直到完成为止。这种方法避免了同步的开销，并且与\emph{fork-join}范式相比更加高效。在大规模网络验证的背景下，大量并行的BDD操作已经充分利用了CPU资源，尝试通过子任务并行来处理单个BDD操作实际上可能会降低性能。采用无中断执行方法有助于提高整体吞吐量，并减少不必要的同步开销。由于每个BDD操作的递归步骤相对较廉价，所以不需要通过\emph{fork-join}的方式来进一步提高单个BDD操作的性能。通过优化整体吞吐量，Nanobdd 在大规模网络验证中能够更高效地处理并行的BDD操作，从而提升验证的效率和性能。
  \item \textbf{可交换哈希函数}。为了优化缓存性能，Nanobdd 采用了一种哈希函数，将可交换的操作映射到相同的哈希值上。例如，$hash(x, \wedge, y) = hash(y, \wedge, x)$。这种设计减少了缓存失效，提升了整体吞吐量。通过使用可交换哈希函数，Nanobdd 确保具有相同语义的BDD操作在缓存中映射到相同的位置，从而增加了缓存的命中率，这样可以更有效地利用缓存，提高系统的整体性能。在大规模数据平面验证中，这种优化对于处理大量的BDD操作非常重要，能够加速验证过程并提高系统的伸缩性。
\end{enumerate}

\textbf{无锁并发的BDD节点表设计。}
本文先对当前已有BDD库的设计进行了调研，图~\ref{fig:bdd-old-table} 为传统BDD节点表（如JDD~\cite{vahidi2023bdd}和Buddy~\cite{jorn2023buddy}）的设计结构，节点表由一个固定大小为$N$的哈希数组（Hash array）和一个节点数组（Data array）构成。其中哈希数组每个元素存储一个节点数组元素地址（data index），节点数组存储所有的BDD节点，BDD节点通过指针（next）构成单向链表，一个单向链表中的节点具有相同的哈希值。同时，节点数组包含一个指向当前未被占用的元素地址指针（freepos）。当创建新的BDD节点时，系统会在freepos处创建该节点，并将freepos指向下一空闲地址，然后通过节点的哈希值获得与其具有相同哈希值的节点链表，最后通过修改哈希数组对应元素的值和自身next指针的值将新节点插入到该链表中。
\begin{figure}[ht]
  \centering
  \subcaptionbox{传统BDD库节点表设计\label{fig:bdd-old-table}}{
    \includegraphics[width=0.48\textwidth]{model/bdd-old-table.pdf}}
  \subcaptionbox{Nanobdd节点表设计\label{fig:nanobdd-nodetable}}{
    \includegraphics[width=0.48\textwidth]{model/nanobdd-nodetable.pdf}}
  \caption{传统BDD库和Nanobdd节点表设计比较}
  \label{fig:nanobdd-nodetable-cmp}
\end{figure}
% \begin{figure}[]
%   \centering
%   \includegraphics[]{model/bdd-old-table.pdf}
%   \caption{传统BDD节点表设计}
%   \label{fig:bdd-old-table}
% \end{figure}

然而，上述过程在多线程并发情况下会导致数据争用问题，比如同时创建两个BDD节点会因为freepos的争用导致他们被创建到同一个位置。另外，如果同时读和写具有相同哈希值的BDD节点，创建BDD的过程会修改链表结构，可能会导致读取BDD节点发生错误。简单地通过锁机制保护上述过程并不能充分利用系统资源，尤其在数据平面验证场景下，大量的BDD操作使系统不断进行加锁和解锁操作，带来较大的线程切换开销。

为了解决上述问题，相关工作往往采用split-ordered lists~\cite{michael2002high,shalev2006splitordered}来构建哈希表，而split-orderd lists需要保证链表内部有序。Nanobdd的节点表采用类似的设计，使用了多个独立的bucket，与split-orderd lists不同，Nanobdd节点表实现了split-unordered lists，并实现相应的算法实现无锁并发。图~\ref{fig:nanobdd-nodetable} 显示了其具体结构，其中每个bucket存储一个BDD节点链表，同一个bucket中的BDD节点具有相同的哈希值。在并发创建或读取BDD节点时，如果两个节点具有不同的哈希值，则可以并行地在不同的bucket中独立并行执行。

% \begin{figure}[]
%   \centering
%   \includegraphics[]{model/nanobdd-nodetable.pdf}
%   \caption{Nanobdd节点表设计}
%   \label{fig:nanobdd-nodetable}
% \end{figure}

然后需要处理的问题是多个BDD操作发生在同一个bucket中时，如何处理数据争用问题。Nanobdd基于Compare-And-Swap（CAS）~\cite{guerraoui2020efficient}机制实现了无锁（lock-free）的并发读写bucket机制。CAS是一个硬件提供的原子操作，代码~\ref{alg:cas} 列出了CAS的伪代码过程。当需要修改变量$var$为$newval$时，如果变量$var$当前的值是$expected$，则将变量$var$的值修改为$newval$并返回True。否则不改变$var$，同时将$expected$赋值为当前$var$的值并返回False。上述比较过程和修改值的操作在一个原子操作内完成，由CPU硬件提供原子保证。

\begin{algorithm}[]
  \caption{Compare-And-Swap过程}
  \label{alg:cas}
  % \KwIn{$T_d$: 设备$d$的转发信息表}
  \SetKwProg{Fn}{Function}{:}{}
  \Fn{\FuncSty{cas}{($var, expected, newval$)}}{
    \If{$var = expected$}{
      $var \gets newval$\;
      \Return{True}\;
    }
    $expected \gets var$\;
    \Return{False}\;
  }
\end{algorithm}

基于CAS原子操作，Nanobdd使用算法~\ref{alg:nanobdd-nodetable} 实现了无锁并发的节点表读写过程。函数$getOrCreateNode$输入一个BDD节点$node$，如果该节点已经存在则返回已存在的节点，否则将该节点插入到节点表。算法首先获取当前节点链表头$head$，并搜索当前节点链表是否已经存在节点$node$，如果已经存在则直接返回已有节点（L2-5），其中搜索过程在函数$searchNode$中给出（L14-19）。如果未搜索到，则尝试将节点$node$插入到链表头，其中第 7 行$lastHead$记录上一次搜索过的链表位置，从而避免重复搜索。算法通过CAS循环监测当前链表头是否被其他线程修改，如果被修改，则继续从修改后的链表头开始搜索是否插入了同样的节点，并记录本次搜索的开始位置（L8-13）。当CAS插入节点成功，则返回该节点（L13）。

\begin{algorithm}[h]
  \caption{Nanobdd节点表无锁并发读写}
  \label{alg:nanobdd-nodetable}
  \small
  % \KwIn{$T_d$: 设备$d$的转发信息表}
  \SetKwProg{Fn}{Function}{:}{}
  \Fn{\FuncSty{getOrCreateNode}{($node$)}}{
    $head \gets$ head of node list\;
    $out \gets \FuncSty{searchNode}(node, head, Null)$\;
    \If{$out \neq Null$}{
      \Return{$out$}\;
    }
    $node.next \gets head$\;
    $lastHead \gets head$\;
    \While{$\FuncSty{cas}(head, node.next, node) = False$}{
      $out \gets \FuncSty{searchNode}(node, node.next, lastHead)$\;
      \If{$out \neq Null$}{
        \Return{$out$}\;
      }
      $lastHead \gets node.next$\;
    }
    
    \Return{$node$}\;
  }
  
  \Fn{\FuncSty{searchNode}{($node, start, end$)}}{
    \While{$start \neq end$}{
      \If{$start = node$} {
        \Return{$start$}\;
      }
      $start = start.next$\;
    }
    \Return{Null}\;
  }
\end{algorithm}

\textbf{无锁并发的BDD缓存设计。}
BDD缓存主要将BDD操作过程中的中间结果记录下来，之后的BDD操作可以通过缓存直接获得最终计算结果，从而避免重复计算。由于缓存主要目的是为了快速获取已经计算过的结果，且允许有不命中的时候，其读写操作不能有较大开销，否则将得不偿失。Nanobdd使用固定大小的内存空间作为缓存，其结构如图~\ref{fig:nanobdd-cache} 所示。

Nanobdd缓存包含$N$条缓存条目，每条缓存条目为一个元组$\langle refCount, op, left, right, result \rangle$，其中$refCount$为一个原子整数，记录当前该条目正在被多少个线程读取，同时令$refCount = -1$表示该条目正在被某一线程写入，Nanobdd基于该原子变量实现了lock-free的共享锁机制。缓存条目的另外三个元素$op, left, right, result$分别表示BDD操作的操作符、相应的操作数和最终结果，如果为一元操作符，则$right = Null$。

\begin{figure}[]
  \centering
  \includegraphics[]{model/nanobdd-cache.pdf}
  \caption{Nanobdd缓存结构}
  \label{fig:nanobdd-cache}
\end{figure}

已有工作如BeeDeeDee~\cite{lovato2014threadsafe}，Sylvan~\cite{tomvandijk2017sylvan} 采用锁机制来实现缓存读写并发，Nanobdd实现了更高效的无锁算法~\ref{alg:nanobdd-cache}，该算法包括缓存查询（lookup）和插入（insert）两个函数，查询函数输入一个BDD操作的哈希值以及相应的操作符和操作数，返回Null表示缓存未命中，否则返回缓存值。lookup函数首先通过哈希值找到对应的缓存条目，如果该条目还未被赋值，则返回Null（L3-5）。否则尝试通过CAS机制将条目的$refCount$增加一，如果当前条目的$useCount < 0$，则表示该条目正在被某一线程写入，此时直接返回Null（L7-9）。若$refCount$设置成功，则判断该缓存条目是否与操作符和操作数一致，如果一致则返回缓存结果（L10-11），否则通过CAS将缓存条目的$refCount$值减一，并返回Null。insert函数则直接通过CAS判断当前缓存条目是否被某一线程使用，如果$refCount = 0$表示该条目可以被安全覆写，并将缓存条目的$refCount$置为$-1$，从而确保写入缓存时不会有其他线程对该缓存条目进行读写，写入完毕后重新将该缓存条目的$refCount$置为0（L16-24）。

Nanobdd缓存所使用的哈希函数设计考虑了BDD操作的交换律特性，对于符合交换律的操作，如AND、OR、XOR和NOT，使用符合交换律的哈希函数对操作数进行哈希。具体来说，Nanobdd使用了如式~\ref{equ:hash} 所示的两个哈希函数，其中$HASH_{UO}$为顺序无关哈希，$HASH_O$为顺序相关哈希。例如计算$x \wedge y$操作的哈希为$hash(x, y, AND) = HASH_O(HASH_UO(x, y), AND)$，由于$HASH_{UO}(x, y) = HASH_{UO}(y, x)$，因此$hash(x, y, AND) = hash(y, x, AND)$，从而进一步提高缓存的命中率。
\begin{equation}
  \label{equ:hash}
  \begin{split}
  HASH_{UO}(x, y) = (x + y) \times (x + y + 1) / 2 \\
  HASH_O(x, y) = (x + y) \times (x + y + 1) / 2 + x
  \end{split}
\end{equation}

在上层编程接口层面，Nanobdd兼容传统BDD库的BDD操作接口，并基于C++实现了操作符重定义，且应用无需显示处理线程同步过程，线程安全相关操作全部基于无锁并发结构实现，使得基于传统BDD库编写的程序可以无缝切换使用Nanobdd。

% \begin{theorem}
%   \label{thm:hash}
%   给定正整数对$(x_1, y_1)$和$(x_2, y_2)$，如果以集合角度看两个正整数对不相等，则$HASH_{UO}(x_1, y_1) \neq HASH_{UO}(x_2, y_2)$。
% \end{theorem}
% \begin{proof}
%   本文用反证法证明定理~\ref{thm:hash}。如果$HASH_{UO}(x_1, y_2) = HASH_{UO}(x_2, y_2)$，则根据式~\ref{equ:hash}可化简得$
% \end{proof}

\begin{algorithm}[h]
  \caption{Nanobdd缓存无锁并发读写}
  % \small
  \label{alg:nanobdd-cache}
  % \KwIn{$T_d$: 设备$d$的转发信息表}
  \SetKwProg{Fn}{Function}{:}{}
  \Fn{\FuncSty{lookup}{($hash, \var{left}, right, op$)}}{
    $out \gets Null$\;
    $entry \gets CACHE[hash \mod CACHESIZE]$\;
    \If{$entry.result = Null$}{
      \Return{$Null$}\;
    }
    $useCount \gets 0$\;
    \While{$\FuncSty{cas}(entry.useCount, useCount, useCount + 1)$}{
      \If{$useCount < 0$}{
        \Return{$Null$}\;
      }
    }
    
    \If{$entry.left = \var{left}$ \text{and} $entry.right = \var{right}$ and $entry.op = op$}{
      $out \gets entry.result$\;
    }
    $useCount \gets entry.useCount$\;
    \While{$\FuncSty{cas}(entry.useCount, useCount, useCount - 1) = False$}{
      pass\;
    }
    \Return{$out$}\;
  }

  \Fn{\FuncSty{insert}{($hash, node, left, right, op$)}}{
    $entry \gets CACHE[hash]$\;
    $useCount \gets 0$\;
    \If{$\FuncSty{cas}(entry.useCount, useCount, -1)$}{
      $entry.result \gets node$\;
      $entry.left \gets left$\;
      $entry.right \gets right$\;
      $entry.op \gets op$\;
      $entry.useCount \gets 0$\;
    }
  }
\end{algorithm}

% \subsubsection{Nanobdd哈希函数}
% \section{基于拓扑原子谓词的数据平面模型设计}
% 为了解决数据平面模型转发等价类过度划分问题，本文提出一种新的atomic predicates定义和计算方法，称为拓扑原子谓词（TAP: Topological Atomic Predicates）。与已有atomic predicates不同，TAP考虑了predicates之间的拓扑相关性，从而避免了等价类的过度划分。

% \subsection{拓扑原子谓词定义}
% 对于一个数据包头$h=\{b_1,...,b_n\}$，令$\{x_1,...x_n\}$为一个布尔变量集合，本文可以将$h$表示为一个布尔逻辑表达式$p_h = c_1 \wedge c_2 ... \wedge c_n$ （简写为$c_1c_2...c_n$），其中：

% \begin{equation}
%   c_i = \begin{cases}
%     x_i & b_i = 1 \\
%     \bar{x_i} & b_i = 0
%   \end{cases}
% \end{equation}
% 例如，数据包头 1010 表示为布尔逻辑表达式为$x_1\bar{x_2}x_3\bar{x_4}$。

% 与之相应，包头空间$H=\{h_1,...h_k\}$的布尔逻辑表达式为$p_H = \vee_{i=1}^k p_{h_i}$。例如，数据包头 1010 和 1011 构成的包头空间布尔逻辑表达式为$x_1\bar{x_2}x_3\bar{x_4} \vee x_1\bar{x_2}x_3x_4 = x_1\bar{x_2}x_3$。一个predicate $p$对应于一个包头空间$\{h | p(h) = True, \forall h \in \mathbb{H}\}$，给定一个数据包头，本文可以很容易根据该数据包头生成布尔表达式的变量值，进而验证该数据包头是否满足一个布尔表达式，所以本文也将上述布尔表达式称为\textbf{谓词} (predicates)。


% 解决等价类过度划分问题的关键在于找到predicates之间的相关性，该相关性主要由节点之间的连通性以及header space的可达性决定，基于谓词之间的相关性，本文只需要对相关的谓词之间求原子谓词即可。令$Path(x \rightarrow y)$表示从设备x到设备$y$的所有路径集合，且$path \in Path(x \rightarrow y)$为其中一条路径，该路径包含从设备$x$到设备$y$通过的链路集合$path = \{(x \rightarrow w_1), (w_1 \rightarrow w_2),...,(w_n \rightarrow y)\}$。

% \begin{definition}
%   Reachable predicates。对于任意两条边$e_i,e_j \in E$，从$e_i$到$e_j$的reachable predicates为$RP(e_i \rightarrow e_j) = \{\bigwedge_{e \in path}p_e \wedge p_{e_i} \wedge p_{e_j}|path \in Path(dst(e_i) \rightarrow src(e_j))\}$。
% \end{definition}

% \begin{definition}
%   Live predicates。给定网络中的一条有向边$e \in E$, $e$的live predicates为$LP_e = \{reach(e \rightarrow e')|e' \in E\}$。其中$reach(e \rightarrow e')$表示从$e$出发可达$e'$的header space。
% \end{definition}

% \begin{definition}
%   拓扑相关谓词（Topologically related predicates）。 令$p_{i \rightarrow j}$和$p_{u \rightarrow v}$分别为从设备$i$到$j$和$u$到$v$的header spaces，如果$\exists path \in Path(j \rightarrow u): \bigwedge_{e \in path}p_e \wedge p_{i \rightarrow j} \wedge p_{u \rightarrow v} \neq False$，或者$\exists path \in Path(v \rightarrow i): \bigwedge_{e \in path}p_e \wedge p_{i \rightarrow j} \wedge p_{u \rightarrow v} \neq False$，则$p_{i \rightarrow j}$和$p_{u \rightarrow v}$拓扑相关，表示为$p_{i \rightarrow j} \sim p_{u \rightarrow v}$。
% \end{definition}


% \begin{definition}
%   拓扑原子谓词 (TAP: Topological atomic predicates)。给定一个网络$G(V, E)$，令$\mathcal{P} = \{p_e | e \in E\}$为link-local predicates，对于任一条边$e \in E$, 其拓扑原子谓词集合$P_e=\{p_1,...,p_k\}$满足以下条件：
% \end{definition}
% \begin{enumerate}
%   \item $p_i \neq False, \forall i \in \{1,...,k\}$;
%   \item $\vee_{i=1}^k p_i = p_e$;
%   \item $p_i \wedge p_j = False, i \neq j$;
%   \item 令$S_e=\bigcup_{e' \in E}(RP(e \rightarrow e') \cup RP(e' \rightarrow e))$，对于$S_e$中的每个predicate $p \in S_e$, $p$可以表达为$P_e$一个子集的合取：$p = \vee_{i\in sub(P_e)}p_i$，其中$sub(P_e)\subseteq \{1,...,k\}$;
%   \item $k$为满足上述条件的最小值。
% \end{enumerate}

% \begin{lemma}
%   \label{lem:equal-gap}
%   在基于拓扑原子谓词构建的数据平面模型$G(V,E,\Sigma)$上进行的验证与在以基于AP构建的模型$G(V,E,AP(\mathcal{P}))$上进行的验证具有相同的结果。
% \end{lemma}
% \begin{proof}
%   为了证明定理~\ref{lem:equal-gap}，本文需要证明对于任何等价类 $p \in GAP$（其中$GAP$ 是全局原子谓词），它从任何边缘 $e \in A$ 进入网络时，两个模型会给出相同的转发图。如果不是这样的话，设 $v$ 是转发图中将 $p$ 从 $e$ 转发到另一个边缘 $e'$ 的交换机。这意味着 $LEP(e, e') \neq emptyset$，但是 $GAP$ 的真相是 $p$ 不会被转发到 $e'$，这与 $LEP$ 的定义相矛盾。
% \end{proof}

% \begin{lemma}
%   TAP实现了最优的数据平面模型。给定一条边 $e \in E$，$|AP(S_e)|$ 是区分穿过 $e$ 的头部空间所需的最小数量。
% \end{lemma}
% \begin{proof}
%   如果任何 $p \in AP(S_e)$ 都不是有用的，那么这意味着 1）上游从未向 $e$ 发送 $p$，并且 2）$p$ 从未在 $e$ 的下游中使用。然而，根据 LEP 的定义，上述两种情况不会发生。
% \end{proof}

% \subsection{基于拓扑原子谓词的数据平面模型}

% 基于TAP的数据平面模型$M\langle V,A,\Sigma,\delta, \lambda \rangle$定义如下：
% \begin{enumerate}
%   \item $V$和$A$与sec{??}定义一致；
%   \item $\Sigma$为拓扑原子谓词集合；
% \end{enumerate}

% 所以，\textbf{基于拓扑原子谓词构建的数据平面模型是正确且最优的}。

% \subsection{基于TAP的数据平面模型构建方法}
% 基于TAP的数据平面模型构建主要包括以下几个步骤。
% \begin{enumerate}
%   \item 计算本地数据平面转发模型。
%   \item 计算全局数据平面模型。
% \end{enumerate}

% \begin{algorithm}[h]
%   \caption{计算本地数据平面转发模型}
%   \label{alg:compute-local-model}
%   \KwIn{$T_d$: 设备$d$的转发信息表}
%   \SetKwProg{Fn}{Function}{:}{}
%   $fwd \gets False$\;
%   \ForEach{$r \in T_d$}{
%     $hit \gets H_r \wedge \not fwd$\;
%     $p_{(d, r.nh)} \gets p_{(d, r.nh)} \vee hit$\;
%     $fwd \gets fwd \vee H_r$\;
%   }
% \end{algorithm}

% \begin{algorithm}[h]
%   \caption{Distributed LEAP Computation}
%   % \KwIn{$LEP(e_i, e_j)$: The received live edge predicate}
%   \SetKwProg{Fn}{Function}{:}{}
%   \Fn{{INIT}{$(v)$}}{
%       \ForEach{$(e, e') \in E^{in}(v) \times E^{out}(v)$}{
%           $LEP_{e, e'} \gets P_{e'}$\;
%           $S_{e'} \gets \{LEP_{e, e'}\}$\;
%           send $LEP_{e, e'}$ to $dst(e')$\;
%       }
%   }
%   \Fn{{OnRecvLEP}{$(LEP_{e_i, e_j})$}}{
%       \If{$e_i \in E^{out}(v)$}{
%           $S_e \gets S_e \cup LEP_{e_i, e_j}$\;
%       }\Else{
%           \ForEach{$e \in E^{out}(dst(e_j))$}{
%               $LEP_{e_i, e} \gets LEP_{e_i, e_j} \wedge P_e$\;
%               $S_e \gets S_e \cup LEP_{e_i, e}$\;
%               % $LEAP(e) \gets AP(S_e)$\;
%               send $LEP_{e_i, e}$ to $dst(e)$ and $src(e_i)$\;
%           }
%       }
%   }
% \end{algorithm}



\section{实验设计和结果分析}
\label{sec:model-eval}
为了评估Flash构建数据平面模型的效果，实验在不同规模的真实数据集上对Flash的FIMT功能进行了评估，通过实验主要回答以下问题：
\begin{enumerate}
  \item Flash的批处理过程是否能够提高数据平面模型构建的吞吐量？
  \item Flash的并行流水线结构是否能够提高系统的伸缩性？
\end{enumerate}

\subsection{系统实现}

\textbf{Flash系统实现。}Flash系统由约4,000行Java代码编写~\footnote{https://github.com/snlab/flash}，基于OpenJDK v17.0.3及以上版本提供的Java API和编译器进行编译。Flash默认采用JDD~\cite{vahidi2023bdd}作为底层BDD操作库，由于JDD仅支持单线程BDD操作，后文中用Flash或Flash (ST)表示该版本的Flash实现。为了集成Nanobdd进而实现并行流水线数据平面模型构建，用C++对核心逻辑进行了实现，将其命名为Flash (PA)。

\textbf{Delta-net和APKeep实现。}
实验将Flash与两个已有的数据平面验证系统Delta-net~\cite{horn2017deltanet}和APKeep~\cite{zhang2020apkeep}进行比较，因为它们是已有工作中最新的，并且经过评估结果显示具有较好性能。同时，实现细节上对Delta-net和APKeep进行了优化，并确保它们与Delta-net~\cite{horn2017deltanet}和APKeep~\cite{zhang2020apkeep}中报告的数据集上具有类似的结果。
\begin{enumerate}
\item
  \textbf{Delta-net}$^*$：
  由于无法获得其源代码，实验按照Delta-net~\cite{horn2017deltanet}中的伪代码实现了Java编写的Delta-net，在结果中使用\textbf{Delta-net}$^*$来表示实验所使用的系统实现。
\item
  \textbf{APKeep}$^*$：与Delta-net类似，APKeep也没有开源实现，使用根据APKeep~\cite{zhang2020apkeep}文献中的伪代码实现APKeep，并使用\textbf{APKeep}$^*$来表示使用所使用的实现。另外，在评估中使用默认的“延迟合并”参数（即：delay=0）。
\end{enumerate}



\subsection{Flash批处理构建数据平面模型效果评估}

\textbf{实验设计。}
实验所使用的数据集如\cref{tab:settings}所示，其中LNet数据集拓扑来自真实的Facebook一个数据中心~\cite{andreyev2014introducing}，基于该数据集生成了不同类型的FIB结构，比如\evalSettingFBzST 表示利用All-pair-shortest-path生成，而\evalSettingFBzST Subspace表示对数据集按照Pod进行包头空间划分后一个分区的数据集。其他类型的数据集包括\evalSettingAirtelST ，\evalSettingStanfordST 和\evalSettingIST 来自于开源数据集。\cref{tab:settings} 同时列出了数据集所对应的拓扑规模和FIB规模，其中$|V|$和$|E|$分别表示拓扑中网络设备的数量和链接数量，FIB规模表示所有设备的FIB规则数量总和。


\begin{table*}
  \caption{实验所使用的数据集}
  \label{tab:settings}
  \centering
  \footnotesize
  \begin{tabular}{|c|c|c|c|c|}
    \hline
    \multirow{2}{*}{\textbf{数据集名称}}
    & \multicolumn{2}{c|}{\textbf{拓扑}}
    & \multirow{2}{*}{\textbf{FIB 生成}}
    & \multirow{2}{*}{\textbf{FIB 规模}}
    \\
    \cline{2-3}
    & 名称 & $|V|/|E|$ & &
    \\\hline
    \makecell*[c]{\evalSettingFBzST Subspace \\ \hline \evalSettingFBzST}
    & \multirow{3}{*}{LNet}
    & \multirow{3}{*}{\makecell{6,016 /\\ 43,008}}
    & \makecell*[l]{StdFIB: 从每个设备到与ToR\\相连的终端设备的最短路径}
    & \makecell*[c]{$2.9 \times 10^5$ \\ \hline $3.2 \times 10^7$}
    \\\cline{1-1}\cline{4-5}
    \makecell*[c]{\evalSettingFBoST Subspace \\ \hline \evalSettingFBoST}
    &
    &
    & \makecell*[l]{StdFIB*: \\具有ECMP规则的StdFIB}
    & \makecell*[c]{$1.2 \times 10^6$ \\ \hline $3.7 \times 10^7$}
    
    
    \\\cline{1-1}\cline{4-5}
    \makecell*[c]{\evalSettingFBsST Subspace \\ \hline \evalSettingFBsST}
    &
    &
    & \makecell*[l]{具有后缀匹配规则的StdFIB*}
    & \makecell*[c]{$3.3 \times 10^5$ \\ \hline $3.7 \times 10^7$}
    
    
    \\\cline{1-5}
    \evalSettingAirtelST
    & Airtel 1
    & 68 / 260
    & \multirow{3}{*}{{\makecell[l]{开源数据集}}}
    & $6.89 \times 10^4$
    
    \\\cline{1-3}\cline{5-5}
    \evalSettingStanfordST
    & Stanford
    & 16 / 37
    &
    & $3.84 \times 10^3$
    
    \\\cline{1-3}\cline{5-5}
    \evalSettingIST
    & Internet2
    & 9 / 28
    &
    & $1.26 \times 10^5$
    
    \\\hline
  \end{tabular}
\end{table*}

\textbf{实验结果。}
首先对Delta-net$^*$、APKeep$^*$和Flash在大规模网络(\evalSettingFBoST 和\evalSettingFBsST )上进行了评估，以展示Flash的整体性能提升。在基准评估中，通过按随机顺序输入所有交换机的规则插入来生成更新，将更新序列提供给验证器，并测量构建逆模型的执行时间和内存消耗。如果执行时间超过10小时，将终止JVM。\cref{fig:pl}显示了结果：Flash (绿色)在\evalSettingFBoST 和\evalSettingFBsST 上分别在19秒和4秒内完成，而Delta-net$^*$ (蓝色)和APKeep$^*$ (橙色)都无法在10小时内完成。因此，对于\evalSettingFBsST ，Flash的性能优于Delta-net*和APKeep$^*$，速度快了9,000倍（10小时除以4秒）。从吞吐量的角度来看，Flash最高可以实现9,250,000 ups（Updates per second），而APKeep*和Delta-net*仅可以实现不超过1,028 ups。另外，Flash的内存消耗也明显较低（在两个实验设置中内存消耗差距高达2个数量级）。虽然该实验设置似乎极端，但在验证器初次启动或按需运行时（例如，用于网络规划~\cite{liu2017crystalnet, zhang2022differential} 或虚拟专用云的可达性分析~\cite{awsdocumentation2022what}）确实会发生。因此，得出结论：Flash在大规模网络中能够实现高效数据平面模型构建且具有较低的内存消耗。

\begin{figure}
  \centering
  \includegraphics[width=\linewidth]{model/baseline.pdf}
  \caption{数据平面模型构建时间以及内存消耗}
  \label{fig:pl}
\end{figure}

然后，实验分析了FIMT作为独立的模型构建方法的好处，由于子空间划分在大型网络中可以广泛有效，实验将子空间划分的思想应用于Delta-net$^*$和APKeep$^*$。除了执行时间和内存消耗，实验计算了每个评估设置中的谓词操作的数量。\Cref{tab:eval-overall-time} 和\cref{tab:eval-overall-mem} 的上方三行显示了结果。例如，名称为\evalSettingFBsST Subspace的行显示了在\evalSettingFBsST 中应用子空间划分的结果。可以观察到，Delta-net*和APKeep$^*$的模型更新时间较长，在\evalSettingFBoST 中分别是Flash的1.4倍（26秒/19秒）和>1,895倍，以及在\evalSettingFBsST 中分别是71倍（285秒/4秒）和251倍。在这两个设置中，Flash的内存占用也较小。例如，在\evalSettingFBsST 中，Flash使用15MB的内存，而Delta-net$^*$和APKeep$^*$分别使用6,792MB和31MB内存。除了\evalSettingFBzST Subspace设置外，Flash还大幅减少了谓词操作的数量（在\evalSettingFBoST 中分别减少了20倍/681倍，而在\evalSettingFBsST 中减少了26倍/4倍）。

为了完整起见，实验接下来使用较小的网络进行评估，并报告了相关文献中广泛使用的三个数据集的结果：\evalSettingAirtelST~\cite{horn2017deltanet}、\evalSettingStanfordST~\cite{kazemian2012header}和\evalSettingIST~\cite{observatory2021internet2}。 \Cref{tab:eval-overall-time} 和\cref{tab:eval-overall-mem} 的最后3行显示了结果。可以看到，APKeep$^*$的模型更新时间是Flash的4.8-6.5倍。在这种较小的网络中，Delta-net$^*$表现最佳，其模型更新时间仅为Flash的30-90\%。这在一些大型网络中也成立，例如\evalSettingFBzST Subspace。然而，Delta-net$^*$的谓词操作数量较高（在\evalSettingAirtelST 中高达141倍）。Delta-net$^*$的高效性来自于其简单高效的数据结构，适用于基于前缀的规则。然而，对于非前缀规则，这种表示法可能会导致性能显著下降，如\evalSettingFBsST 和\evalSettingFBoST 的结果所示，类似的性能下降结果也在APKeep~\cite{zhang2020apkeep}中报告过。

根据实验结果，可以得出以下结论：Flash在各种拓扑结构和FIB更新设置下都具有稳定的快速性能。在具有大型网络和复杂的转发行为的设置中（例如\evalSettingFBsST 和\evalSettingFBoST ），Flash相比现有技术取得了显著的性能提升。

\begin{table*}
    \caption{对包头空间划分后数据平面模型的构建时间}
    \label{tab:eval-overall-time}
    \footnotesize
    \newcommand\best[1]{{\bfseries#1}}
    \centering
    \begin{tabular}{|c|c|c|c|c|c|}
      \hline
      \multirow{2}{*}{数据集}
      & \multicolumn{3}{c|}{数据平面模型构建时间 (s)}\\
      \cline{2-4}
      
      & Delta-net$^*$ (提升比) & APKeep$^*$ (提升比) & Flash  \\
      \hline
      \evalSettingFBzST Subspace
      & \best{0.7} (0.3$\times$) & 34.1 (15$\times$) & 2.3  \\
      \evalSettingFBoST Subspace
      & 26 (1.4$\times$) & > 36,000 (>1,895$\times$) & \best{19}\\
      \evalSettingFBsST Subspace
      & 285 (71$\times$)   & 1,004 (251$\times$) & \best{4}  \\
      \hline
      \evalSettingAirtelST
      & \best{12} (0.9$\times$) & 85 (6.5$\times$) & 13\\
      \evalSettingStanfordST
      & \best{0.06} (0.5$\times$) & 0.58 (4.8$\times$) & 0.12\\
      \evalSettingIST
      & \best{0.4} (0.3$\times$) & 6.9 (4.9$\times$) & 1.4\\
      \hline
    \end{tabular}
  \end{table*}

\begin{table*}
  \caption{对包头空间划分后数据平面构建的内存消耗和谓词操作规模}
  \label{tab:eval-overall-mem}
  \footnotesize
  \newcommand\best[1]{{\bfseries#1}}
  \centering
  \begin{tabular}{|c|c|c|c|c|c|c|c|c|}
    \hline
    \multirow{2}{*}{数据集}
    & \multicolumn{3}{c|}{内存开销 (MB)}
    & \multicolumn{3}{c|}{\# 谓词操作 ($10^5$)} \\
    \cline{2-7}
    
    & Delta-net$^*$ & APKeep$^*$ & Flash
    & Delta-net$^*$ & APKeep$^*$ & Flash  \\
    \hline
    \evalSettingFBzST Subspace
    & \best{29} & 66 & 55
    & \best{6} (0.4$\times$)   & 71 (5$\times$)    & 14  \\
    \evalSettingFBoST Subspace
    & 1,249 & > 1,096 & \best{211}
    & 281 (20$\times$) & > 9,529 (681$\times$)    & \best{14}\\
    \evalSettingFBsST Subspace
    & 6,792 & 31  & \best{15}
    & 1,485 (26$\times$) & 239 (4$\times$)     & \best{57} \\
    \hline
    \evalSettingAirtelST
    & \best{5}    & 37  & 70 
    & 141 (141$\times$)       & 1,321 (1,321$\times$) & \best{1}\\
    \evalSettingStanfordST
    & \best{3}    & 9   & 9
    & \best{1} (1$\times$)  & 4.3 (4.3$\times$) & \best{1}\\
    \evalSettingIST
    & \best{16}   & 52  & 52
    & 4 (2$\times$)            & 56 (28$\times$)   & \best{2}\\
    \hline
  \end{tabular}
\end{table*}

为了更好地理解MR2对Flash整体性能提升的贡献，实验对模型构建过程中的三个阶段进行了详细分析：计算原子覆写（Map）、原子覆写聚合（即Reduce I/II）和数据平面模型更新。测量了APKeep$^*$、Flash和Flash的一个变种，称为Flash PUM（per-update mode, PUM）在每个阶段的总时间。

\cref{fig:i2-breakdown}展示了\evalSettingIST 设置下APKeep$^*$、Flash（PUM）和Flash各阶段的时间分解情况。虽然Flash在原子覆写聚合阶段引入了一些开销（0.42秒），但与APKeep$^*$相比，计算原子覆写的时间缩短了3.85倍，数据平面模型更新的时间缩短了12.3倍。需要注意的是，在Flash（PUM）中，数据平面模型更新的时间（4.84秒）比APKeep$^*$（4.55秒）更长，因为数据平面模型更新的交叉积计算阶段对单个规则更新没有进行优化。因此，得出结论：通过原子覆写聚合，MR2使得Flash能够大幅减少计算原子覆写和聚合原子覆写的时间，从而提升了性能。

\begin{figure}
  \centering
  \includegraphics[width=0.8\linewidth]{model/i2-teardown.pdf}
  \caption{\evalSettingIST 数据平面模型构建时间分析}
  \label{fig:i2-breakdown}
\end{figure}

% \begin{table}[htp]
%   \center
%   \caption{GAP和TAP比较使用的数据集}
%   \label{tab:leap-datasets}
%   \begin{tabular}{|c|c|c|c|c|}
%     \hline
%     \emph{Dataset}
%     & \emph{\#Nodes}
%     & \emph{\#Links}
%     & \emph{\#Rules}
%     & \emph{\#GAP}
%     \\\hline
%     Internet2 & 9 & 28
%     & $1.26 \times 10^5$ & 216
%     \\\hline
%     Stanford & 16 & 37
%     & $7.59 \times 10^5$ & 494
%     \\\hline
%     Airtel1 & 68 & 260
%     & $4.84 \times 10^4$ & 16
%     \\\hline
%     Airtel2 & 68 & 260
%     & $9.85 \times 10^4$ & 1,401
%     \\\hline
%     Berkeley & 23 & 252
%     & $1.28 \times 10^7$ & 540
%     \\\hline
%     INET & 315 & 40,770
%     & $1.25 \times 10^8$ & 7,984
%     \\\hline
%     RF1755 & 87 & 2,308
%     & $3.37 \times 10^7$ & 26,638
%     \\\hline
%     RF3257 & 161 & 9,432
%     & $7.45 \times 10^7$ & 556,121
%     \\\hline
%     RF6461 & 138 & 8,140
%     & $7.50 \times 10^7$ & 594,641
%     \\\hline
%   \end{tabular}
% \end{table}

\subsection{Flash并行流水线构建数据平面模型效果评估}
\textbf{实验设计。}
为了评估Flash并行流水线执行效果，在\cref{tab:settings}中所示的数据集上运行了具有并行流水线功能的Flash，命名为Flash (PA)，同时与Delta-net*, APKeep*以及Flash的单线程模式Flash (ST)进行比较。

\textbf{实验结果。}
\cref{fig:model-par}所示为Flash并行流水线执行的实验结果，X轴为\cref{tab:settings}中对应的数据集，Y轴为使用不同系统的数据平面模型构建时间。可以得出以下结论：1）相比单线程Flash，Flash并行流水线执行能够提供2-10倍的速度提升；2）在启用Subspace划分后，相比已有工作，Flash能够实现最高超过17,000倍的速度提升（LNet-ecmp-Subspace）；3）相比无Subspace的情况下，结合\cref{fig:pl}所示的结果，相比已有工作，Flash能够实现最高约40,000倍的速度提升（LNet-smr Subspace）。

\begin{figure}
  \centering
  \includegraphics[width=0.8\linewidth]{figures/model/nanobdd.pdf}
  \caption{Flash并行流水线效果}
  \label{fig:model-par}
\end{figure}

Flash相比已有工作之所以能够实现进一步的效率提升，主要取决于两方面因素：首先，Flash的批量化处理过程能够消除大部分冗余更新，同时能够对更新进行聚合，从而降低了系统的输入规模，在大规模网络中，能够将数据平面模型构建效率提升近9,000倍；另一方面，并行流水线方式能够并发的对多个数据平面更新进行并发处理，在本实验环境下实现2-10倍速度提升。综合两方面因素，Flash相比已有工作在本文所设置的环境中实现40,000倍速度提升。

\section{本章小结}
本章着重研究了针对大规模网络的数据平面模型构建。首先通过分析大规模网络中普遍存在的“更新风暴”问题，提出了如何提高数据平面模型构建的吞吐量和伸缩性问题。然后深入研究了与“更新风暴”相关的数据平面更新问题，特别关注了非原子性和谓词并发操作方面的挑战。随后，引入了面向大规模网络的数据平面验证系统Flash。Flash采用了快速逆模型变换（FIMT）和并行流水线的数据平面模型构建方法，旨在提高构建数据平面模型的效率。最后，通过在真实大规模网络上进行一系列实验，证明了Flash相对于最新的工作，在数据平面模型构建效率方面取得了巨大的提升，效率提高了高达40,000倍。
% 这一系列工作为大规模网络数据平面模型构建提供了创新性的解决方案，有望在网络可靠性和网络验证性能优化方面产生深远的影响。
